[Ur] project to a fieldname list

[Adam Chlipala]

Gergely Buday wrote:
> my idea is to write a function that projectds records to a given set
> of names. Is it doable in Ur/Web?
>    

I'm not sure exactly what you're asking for.  Does the [---] operator do 
the trick?  Its first argument is a value of record type, and its second 
argument is a constructor of kind [{Type}], specifying which fields to 
remove from the record.

> My preliminary attempt is to fix the type of it:
>
> con roles :: {Unit}  = [1, 2, 3]
>
> fun projection [ r ::: {Type} ] (names :: {Unit}) (record : $r) : (map
> (fn nm =>  record.nm) names) = ()
>
> [gergoe at homeship sandbox]$ urweb books
> books.ur:3:43-3:47: syntax error: replacing  KUNIT with  DOTDOTDOT
> books.ur:3:87-3:88: syntax error: replacing  DOT with  COMMA
>
> What is the problem with {Unit}, syntactically?

You probably meant to enclose [names] and its kind in square brackets, 
not parens.

> And, with the dot as a field operator?
>    

The return type is fundamentally nonsensical, because it mentions 
[record], a value.  Ur isn't dependently typed, so you can never mention 
value-level variables in types.  At the type level, [.] means something 
different, and its second argument must always be a numeral.  (It's for 
projection from constructors of tuple kinds.)