[Ur] record expression

[Adam Chlipala]

Gergely Buday wrote:
> is it possible to write in Ur a type definiton that expresses that
>
> type myRecord = { MyField : int, MyOtherField : string,
>                              and here come some identically typed fields,
>                              1:  $((First : option price, Second :
> option price) ++ map option otherFields),
>                              2:  $((First : option price, Second :
> option price) ++ map option otherFields)
>                                  ...
>                              n: $((First : option price, Second :
> option price) ++ map option otherFields)
>                             }
>
> where n is not fixed at the time of the writing but depends on other
> definitions?
>    

I would do it as:

type copiedType = float (* fill something else in here *)

con copiedFields = [1, 2, 3] (* fill something else in here *)

type myRecord = $([MyField = int, MyOtherField = string] ++ mapU 
copiedType copiedFields)


You could make this abstraction first-class as a type-level function, 
but that would require including a disjointness obligation, which would 
complicate use of such types.