[mercury-users] Dependent Types

[Stefan Karrmann]

There is an interesting extension of Haskell by Lennart Augustsson.
It is Cayenne (see http://www.cs.chalmers.se/~augustss/cayenne/index.html)
which uses dependent types. This increases the power of functions, e.g.
you can type printf:

module example$printf =
#include Prelude
struct
concrete
PrintfType :: String -> #
PrintfType (Nil)          = String
PrintfType ('%':('d':cs)) = Int    -> PrintfType cs
PrintfType ('%':('s':cs)) = String -> PrintfType cs
PrintfType ('%':( _ :cs)) =           PrintfType cs
PrintfType ( _ :cs)       =           PrintfType cs

private 
printf' :: (fmt::String) -> String -> PrintfType fmt
printf' (Nil)          out = out
printf' ('%':('d':cs)) out = \ (i::Int)    -> printf' cs (out ++ show i)
printf' ('%':('s':cs)) out = \ (s::String) -> printf' cs (out ++ s)
printf' ('%':( c :cs)) out =                  printf' cs (out ++ c : Nil)
printf' (c:cs)         out =                  printf' cs (out ++ c : Nil)

printf :: (fmt::String) -> PrintfType fmt
printf fmt = printf' fmt Nil

Can Mercury be extended in a similar way? How would it look like?

Thanks,
-- 
Stefan Karrmann
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------