On 12/24/2014 08:26 PM, Stefan Scott Alexander wrote:
Right now I'm experimenting with 'eq' (which I assume tests whether
two lists are equal) and I'm getting parse errors, for something
(supposedly) simple like:
val nums1 = 1 :: 2 :: 3 :: []
val nums2 = 101 :: 102 :: 103 :: []
eq nums1 nums2
This code doesn't parse the way you think. It's not allowed to have
several declarations followed by a freestanding expression. The grammar
in the Ur/Web manual should give all the details, but changing the last
line like so would at least lead to a parse more likely to be what you
expect:
val eq_result = eq nums1 nums2
Your code above actually tries to put the [eq] call onto the end of the
value of [nums2]!
Also, [x = y] is syntactic sugar for [eq x y]. It would not be normal
to write [eq] explicitly like above.
Would it be correct for me to call 'eq' a "library function" - or is
it actually something else (perhaps something involving type classes)?
[eq] in the initial environment is a type-class-parameterized function.
The same name happens to be reused for a different purpose in the List
module.
(1) Here is the signature of the (library function? type class?) 'eq'
in list.urs:
datatype t = datatype Basis.list
val eq : a ::: Type -> eq a -> eq (t a)
This is a rule for concluding that [list a] belongs to the [eq] type
class if [a] belongs to it. It's not a function that you'd call to test
equality of lists. Just compare two lists with infix operator [=] like
Joe Average Programmer would expect, and everything should work, if the
List module is in scope.
(2) Here is (part of) the signature of (library function?) 'eq' in
basis.urs:
class eq
val eq : t ::: Type -> eq t -> t -> t -> bool
I believe the above two lines from basis.urs are saying: "'eq' is a
function (defined for Type t, where t admits equality - similar to
type classes in Haskell), which takes two arguments of Type t, and
returns a bool."
Yes, type classes are exactly what's going on here.
(3) And here is the definition of the library function 'eq' in list.ur:
val eq = fn [a] (_ : eq a) =>
let
fun eq' (ls1 : list a) ls2 =
case (ls1, ls2) of
([], []) => True
| (x1 :: ls1, x2 :: ls2) => x1 = x2 && eq' ls1 ls2
| _ => False
in
mkEq eq'
end
The recursive part in the above definition, involving the three
pattern-matchings, seems quite clear and standard.
However, there are several other things which are confusing:
- Why is there a "don't care" wildcard for the second argument on the
first line?
Type class quantification in Ur works by passing explicit witness
objects. Instance resolution uses them automatically as needed, hence
there is no need to assign names to those parameters.
- Why do the two args on the first line look so different? I would
expect 'eq' to take two args of the same type
I hope my earlier answer helps: this is a definition of an inference
rule for type classes, not an equality-testing function.
However, I can't find the definition of mkEq anywhere - only its
signature - so I have no idea what mkEq does.
It's the function to be used in creating new instance witnesses for the
[eq] type class.
- The first argument ls1 to eq' is declared to be of type 'list a'.
Why is there no similar declaration for the second argument, ls2?
(Maybe there is some type inference going on?)
Yes, type inference does it.
Am I going about this all wrong? Should I be starting by reading some
simpler documentation on SML or something? I would welcome any
suggestions. Thanks!
All of the Ur/Web documentation does assume serious familiarity with
both Haskell and some ML language.
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
