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."
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
