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