Yes, the Agda modules remind me of Cayenne. :)
On Tue, Jan 20, 2009 at 12:54 PM, Bas van Dijk <[email protected]> wrote: > On Wed, Jan 14, 2009 at 3:59 PM, Manlio Perillo > <[email protected]> wrote: >> 2) In Python it is possible to import modules inside a function. >> >> In Haskell something like: >> >> joinPath' root name = >> joinPath [root, name] >> importing System.FilePath (joinPath) > > I just like to point out the dependently typed, Haskell-like, > programming language Agda[1] which has a very nice module system with > the following features: > > * Modules can contain other modules > > * Modules can be locally opened. For example: > mapMaybe f m = let open Maybe in maybe nothing (just . f) m > > * Renaming of important names: For example: > open Maybe renaming (Maybe to option; nothing to none; just to some) > > * Parameterized modules: For example: > > module Sort (A : Set) (_<_ : A -> A -> Bool) where > insert : A -> List A -> List A > insert y [] = y :: [] > insert y (x :: xs) with x < y > ... | true = x :: insert y xs > ... | false = y :: x :: xs > > See section 2.7 of the following Agda tutorial (an open minded Haskell > hacker should be able to read that section on its own): > > http://www.cs.chalmers.se/~ulfn/darcs/AFP08/LectureNotes/AgdaIntro.pdf > > Hopefully Haskell can borrow some of these ideas sometime. > > regards, > > Bas > > [1] http://wiki.portal.chalmers.se/agda/ > _______________________________________________ > Haskell-Cafe mailing list > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
