-- M.agda ------------
open import Relation.Binary using (Setoid; module Setoid)
open import Data.Nat using (ℕ)
h : ℕ
h = 0
module M {α α=} (A : Setoid α α=)
where
open Setoid A
f : Carrier → ℕ
f _ = 0
module _ (B : Set) where
g : B → ℕ
g _ = 0
-----------------------------------------On Wed, Aug 5, 2015 at 9:55 AM, Oliver Charles <ollie@ocharles.org.uk> wrote:
> It makes me sad if we can't progress the language on the grounds that
> people's attempts at parsing the source code themselves would break. If you
> want to know all the imports, then we should be providing this information
> through tools for people to consume.
It's not whether or not there's a tool, there already is. It's that
the tool must be more complicated. For example, we can get imports
from haskell-src-exts but it has bugs, it can be out of date, and it's
slower. Or ghc -M... which doesn't have those problems. So maybe
it's not really a serious objection.
>> On the other hand, lots of languages have a "local open" feature like
>> this. I think many of them make you first import the module, and then
>> you can "open" it in a local scope. This would address both my "parse
>> the whole file for imports" objection and the "what about instances",
>> because module importing would be unchanged.
>
> Indeed, this could be a path forward. I'm not really familiar with any
> languages that do this, could you link to some examples of how this works in
> other languages?
I was thinking of agda.. though it's only from memory so I could be
wrong. Or perhaps it was cayenne... one of those dependently typed
languages models modules as records, and then has syntax to dequalify
record access. Rust has a full-on nested module system, but I seem to
recall you have to declare a link dependency on an external crate
("import"), and then separately import the symbols from it ("use").
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe