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

[Adam Chlipala]

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."