[Ur] Compile error in simple test app involving 'list' and 'eq'; difficulty understanding higher-order expressions

[Adam Chlipala]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.impredicative.com/pipermail/ur/attachments/20141224/7a7d0728/attachment-0001.html>