[Ur] simple example about constructing rects - guarded types?

Adam Chlipala adamc at impredicative.com
Mon Dec 20 09:03:28 EST 2010


Marc Weber wrote:
> I want to build a simple type constructor: It takes two names and two
> types and should build the record type {name1 = type1, name2 = type2}
>
> [...]
>
> So how to fix is? Is this a case where guarded types must be used?
>    

Yes, though it requires a slight change of perspective.  The Ur type 
system doesn't support type-level functions with disjointness 
obligations.  The best you can do is return a type that has some 
disjointness obligations left over, which, in general, won't be so much 
fun.  Still, here's my answer that comes closest to your original question:

con build_record = fn (a::Name) (b::Name) (c::Type) (d::Type) => [[a] ~ 
[b]] => {a : c, b : d}

Here's an example of a value-level function to build a two-field record, 
which has nicer behavior.

fun twor [a :: Name] [b :: Name] [[a] ~ [b]] [c :: Type] [d :: Type] (x 
: c) (y : d) : {a : c, b : d} =
     {a = x, b = y}

You _can_ use the [build_record] function, but notice how it forces you 
to begin the body with the same disjointness abstraction from the 
definition of [build_record]:

fun twor' [a :: Name] [b :: Name] [c :: Type] [d :: Type] (x : c) (y : 
d) : build_record a b c d =
     fn [[a] ~ [b]] => {a = x, b = y}

> Also looking at this example:
> http://impredicative.com/wiki/index.php/Using_Top.Fold_to_count_fields_of_a_record:
>
>    con rr :: {Type} = [One = int, Two = string, Three = bool, Four = list float]
>
>    val q : int = @@fold [fn (rx :: {Type}) =>  (int)]
>                    (fn [nm :: Name] [t :: Type] [r :: {Type}] [[nm] ~ r] acc =>  1 + acc)
>                    (0) [rr] (_ : folder rr)
>
> I don't understand why the arguments of the fn lambda are put in square
> brackets.
>    

The general convention is that type-level arguments of value-level 
functions go in square brackets.

> Is this the "polymorphic function abstraction":
>    lambda [x ? kappa] =>  e
>
> which is listed in the expression section of the manual?
>    

Most of them are.  The last one is an instance of "lambda [c ~ c] => e", 
the disjointness abstraction.  The sugar for this is part of the general 
binder notation described in Section 4.3 of the manual, in the paragraph 
beginning "At the expression level."



More information about the Ur mailing list