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

[Stefan Scott Alexander]

In order to learn UrWeb, I'm defining a simple web page calling some UrWeb
library functions as a vehicle to experiment with these functions and
understand what they do.

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

Would it be correct for me to call 'eq' a "library function" - or is it
actually something else (perhaps something involving type classes)?

I understand that in a statically typed language, a function "eq" which
compares for equality must necessarily be polymorphic. I guess I'm just
having a hard time understanding the notation used for this in UrWeb / SML.

I've done a search through all the UrWeb files to find everything involved
with the definition of 'eq', and found the following:

(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)

I don't understand the rank of 'eq' in the above specification. It seems to
start with a Kind declaration

  a ::: Type

followed perhaps by a type class declaration

  eq a

... but after that, I would expect to see *two* argument types, and finally
a *result* type such as:

  bool

and not just *one* type 'eq (t a)'

So while I understand that the rank must assuredly be correct, as a novice
UrWeb user it seems to me to be two items "short", and I can't understand
this rank.

- Maybe there's some currying going on?

- Or maybe the above rank is saying: "If 'a' is a Kind, and 'a' is of the
type class 'eq' admitting equality, then '(t a)' - ie '(Basis.list a)'
*also* is of the type class 'eq' admitting equality?

(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."

(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?

- Why do the two args on the first line look so different? I would expect
'eq' to take two args of the same type, so I would expect its definition to
show two similar-looking args, instead of the rather radically different
args:

[a]
(_ : eq a)

- Why are there brackets around the first arg? I thought that brackets mean
"an optional type-level argument". If so, then is there only *one*
value-level argument to 'eq' here: the "second" one? But how can that be,
if 'eq' takes two args?

- Maybe there is some way of interpreting the two args above to be somehow
"the same"? - ie, maybe the first one just says "the first arg of 'eq' is
of type 'a'" - and maybe the second one says: "the second arg is *also* of
type 'a' - and by the way, type 'a' has to be in "type class" 'eq a'".
- Where is the linkage between the parameters 'a' of the *outer* function
eq, and the parameters ls1 and ls2 of the inner (auxiliary) function eq'?
(I presume this linkage is somehow established via the call the mkEq.
However, I can't find the definition of mkEq anywhere - only its signature
- so I have no idea what mkEq does. And finally: even if mkEq does somehow
establish a 'linkage' between the parameters of eq' and eq, it seems like
it could still be hard because the second arg of eq was thrown away using a
"don't care" wildcard.

- 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?)

(4) Here is the signature of 'mkEq' in basis.urs:

  val mkEq : t ::: Type -> (t -> t -> bool) -> eq t

I have no idea what 'mkEq' does. Perhaps, being a signature in basis.urs,
its definition is "built-in" and not visible to the user?

---

Here is my file list_test.urp:

  debug

  $/list
  list_test

And here is my file list_test.ur (with the the offending lines involving
'eq' commented out):

  open List

  val nums1 = 1 :: 2 :: 3 :: []
  val nums2 = 101 :: 102 :: 103 :: []

  val fn1 x y = (2 * x) + y
  val minus100 x = x - 100

  fun main () : transaction page =
  return <xml><body>
      <li> val nums1 = 1 :: 2 :: 3 :: []</li>
      <li> val nums2 = 101 :: 102 :: 103 :: []</li>
      <li> val fn1 x y = (2 * x) + y</li>
      <li> foldl fn1 1 nums1 = {[ foldl fn1 1 nums1 ]}</li>
      <li> foldl fn1 1 nums2 = {[ foldl fn1 1 nums2 ]}</li>
      <li> mp minus100 nums2 = {[ mp minus100 nums2 ]}</li>
  (*  <li> eq nums1 nums2 = {[ eq nums1 nums2 ]}</li>  *)
  (*  <li> eq nums1 (mp minus100 nums2) = {[ eq nums1 (mp minus100 nums2)
]}</li>  *)
  </body></xml>

The above works fine (with those two lines commented out), and I can go to
127.0.0.1:8080/List_test/main and see the web page:

  - val nums1 = 1 :: 2 :: 3 :: []
  - val nums2 = 101 :: 102 :: 103 :: []
  - val fn1 x y = (2 * x) + y
  - foldl fn1 1 nums1 = 13
  - foldl fn1 1 nums2 = 613
  - mp minus100 nums2 = 1 :: 2 :: 3 :: []

However, if I uncomment the two lines involving 'eq' and attempt to
compile, doing:

  urweb list_test

I get the following compile errors:

  list_test.ur:17:29: (to 17:31) Unification failure
  Expression:  eq [<UNIF:U543::Type>] _
    Have con:  eq (list <UNIF:U543::Type>)
    Need con:  <UNIF:U544::Type> -> <UNIF:U545::Type>
  Incompatible constructors
  Have:  eq (list <UNIF:U543::Type>)
  Need:  <UNIF:U544::Type> -> <UNIF:U545::Type>

  list_test.ur:18:43: (to 18:45) Unification failure
  Expression:  eq [<UNIF:U628::Type>] _
    Have con:  eq (list <UNIF:U628::Type>)
    Need con:  <UNIF:U629::Type> -> <UNIF:U630::Type>
  Incompatible constructors
  Have:  eq (list <UNIF:U628::Type>)
  Need:  <UNIF:U629::Type> -> <UNIF:U630::Type>

Questions:

(1) Have I misunderstood the rank of 'eq'?

(2) What does 'mkEq' do?

(3) Why are the signatures for 'eq' in basis.urs and list.urs different?

I apologize for these sorts of novice questions. I am only somewhat
familiar with ML and Haskell, only having read some manuals and tutorials.

I do admit I have always had a hard time understanding higher-order
functions - tending to agree with the paper "Higher Order Functions
Considered Unnecessary for Higher Order Programming" by Joseph Goguen
(involved with the languages OBJ3 and Maude) which points out 3 possible
issues with higher-order logic:

  http://cseweb.ucsd.edu/~goguen/pps/utyop.pdf

- "higher order expressions are notoriously difficult for humans to read
and write correctly" (This certainly seems to be applicable to me here: I
can't figure out the rank of a simple function such as 'eq' - possibly due
to (a) the extra args stuck on the front to declare the Kind and the type
class and (b) the seemingly different ranks of 'eq' in (1) and (2)
mentioned at the start of this message.)

- "higher order logic does not mix well with subsorts"

- unlike higher-order languages, first-order languages such as Maude and
OBJ3 (which use 'theories' to parameterize modules) permit imposing axioms
(semantics) on arbitrary functions in those theories (eg, associativity,
commutativity, identity element)

I think it can be interesting to observe that how hard it can be for
certain users to make the transition from first-order algebraic
specification languages such as Maude or OBJ3 to higher-order languages
such as ML and Haskell. I've been trying off and on for years, and making
very little headway - but I keep on trying, because ML and Haskell have
compilers, and useful applications such as UrWeb.

I would assume that UrWeb (and SML) should probably be learnable for
someone who is comfortable using a functional language such as Maude - and
indeed the manuals for SML seem easy enough to read and understand. But
when I try to read non-trivial UrWeb code (such as the Grid1 demo), or even
fairly trivial code (such as the signature and definition of 'eq' in
basis.urs and list.ur and list.urs, as shown above) - I am surprised to
find myself utterly bewildered.

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!

###
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.impredicative.com/pipermail/ur/attachments/20141224/a4446d27/attachment.html>