Proposal: Don't require users to use undefined

Bas van Dijk v.dijk.bas at gmail.com
Fri Oct 29 18:18:44 EDT 2010


On Thu, Oct 28, 2010 at 11:33 AM, Christian Maeder
<Christian.Maeder at dfki.de> wrote:
> ...other languages (like pvs, opal, HasCASL with
> paramterized modules) use optional type arguments in square brackets
> that would clash/overlap Haskell's list syntax.
> ...

This reminds me of Agda's implicit arguments:

See section 2.3 of: http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf

For example:

map : {A B : Set} -> (A -> B) -> List A -> List B
map f [] = []
map f (x :: xs) = f x :: map f xs

foo : List Char -> List Int
foo = map {Char} {Int}

Regards,

Bas

P.S.
This topic is drifting wildly offtopic but I like it ;-) (and we have
some weeks left for the proposal)


More information about the Libraries mailing list