Marc Weber wrote:
http://impredicative.com/ur/tutorial/tlc.html
shows this example:
type nat = t :: Type -> t -> (t -> t) -> t
val zero : nat = fn [t :: Type] (z : t) (s : t -> t) => z
fun succ (n : nat) : nat = fn [t :: Type] (z : t) (s : t -> t) => s (n [t]
z s)
val one = succ zero
val two = succ one
val three = succ two
three [int] 0 (plus 1)
== 3
three [string] "" (strcat "!")
== "!!!"
Eg the succ function has t in its return type and in it n:nat arg.
So should urweb be able to deduce type of t automatically? Should it be
possible to replace the explicit :: by an implicit t ::: Type ?
Trying to do so I get some unification errors - is it because I removed
some [t] like args incorrectly?
You're not far from a correct solution. You just need to use [@@]
prefixes to suppress implicit argument insertion in places where you
want to retain first-class polymorphism.
type nat = t ::: Type -> t -> (t -> t) -> t
val zero : nat = fn [t ::: Type] (z : t) (s : t -> t) => z
fun succ (n : nat) : nat = fn [t ::: Type] (z : t) (s : t -> t) => s (n z s)
val one = @@succ @@zero
val two = @@succ @@one
val three = @@succ @@two
val test1 = three 0 (plus 1)
val test2 = three "" (strcat "!")
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
