<div dir="ltr"><div><span style="font-family:monospace,monospace">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.<br><br>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:<br><br>  val nums1 = 1 :: 2 :: 3 :: []<br>  val nums2 = 101 :: 102 :: 103 :: []<br>  <br>  eq nums1 nums2<br><br>Would it be correct for me to call 'eq' a "library function" - or is it actually something else (perhaps something involving type classes)? <br><br></span></div><span style="font-family:monospace,monospace">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.<br></span><div><span style="font-family:monospace,monospace"><br>I've done a search through all the UrWeb files to find everything involved with the definition of 'eq', and found the following:<br><br>(1) Here is the signature of the (library function? type class?) 'eq' in list.urs:<br><br>  datatype t = datatype Basis.list<br> <br>  val eq : a ::: Type -> eq a -> eq (t a)<br> <br>I don't understand the rank of 'eq' in the above specification. It seems to start with a Kind declaration<br><br>  a ::: Type<br><br>followed perhaps by a type class declaration<br><br>  eq a<br><br>... but after that, I would expect to see *two* argument types, and finally a *result* type such as:<br><br>  bool<br><br>and not just *one* type 'eq (t a)'<br><br>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.<br><br>- Maybe there's some currying going on?<br><br>- 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?<br> <br>(2) Here is (part of) the signature of (library function?) 'eq' in basis.urs:<br><br>  class eq<br>  val eq : t ::: Type -> eq t -> t -> t -> bool<br> <br>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."<br><br>(3) And here is the definition of the library function 'eq' in list.ur:<br><br>  val eq = fn [a] (_ : eq a) =><br>              let<br>                  fun eq' (ls1 : list a) ls2 =<br>                      case (ls1, ls2) of<br>                          ([], []) => True<br>                        | (x1 :: ls1, x2 :: ls2) => x1 = x2 && eq' ls1 ls2<br>                        | _ => False<br>              in<br>                  mkEq eq'<br>              end<br><br>The recursive part in the above definition, involving the three pattern-matchings, seems quite clear and standard.<br><br>However, there are several other things which are confusing:<br><br>- Why is there a "don't care" wildcard for the second argument on the first line?<br><br>- 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:<br><br>[a]<br>(_ : eq a)<br><br>- 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?<br><br>- 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'".<br>- 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.<br><br>- 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?)<br><br>(4) Here is the signature of 'mkEq' in basis.urs:<br><br>  val mkEq : t ::: Type -> (t -> t -> bool) -> eq t<br> <br>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?<br><br>---<br><br>Here is my file list_test.urp:<br><br>  debug<br><br>  $/list<br>  list_test<br><br>And here is my file list_test.ur (with the the offending lines involving 'eq' commented out):<br><br>  open List<br><br>  val nums1 = 1 :: 2 :: 3 :: []<br>  val nums2 = 101 :: 102 :: 103 :: []<br><br>  val fn1 x y = (2 * x) + y<br>  val minus100 x = x - 100<br><br>  fun main () : transaction page =<br>  return <xml><body><br>      <li> val nums1 = 1 :: 2 :: 3 :: []</li><br>      <li> val nums2 = 101 :: 102 :: 103 :: []</li><br>      <li> val fn1 x y = (2 * x) + y</li><br>      <li> foldl fn1 1 nums1 = {[ foldl fn1 1 nums1 ]}</li><br>      <li> foldl fn1 1 nums2 = {[ foldl fn1 1 nums2 ]}</li><br>      <li> mp minus100 nums2 = {[ mp minus100 nums2 ]}</li><br>  (*  <li> eq nums1 nums2 = {[ eq nums1 nums2 ]}</li>  *)<br>  (*  <li> eq nums1 (mp minus100 nums2) = {[ eq nums1 (mp minus100 nums2) ]}</li>  *)<br>  </body></xml><br><br>The above works fine (with those two lines commented out), and I can go to <a href="http://127.0.0.1:8080/List_test/main">127.0.0.1:8080/List_test/main</a> and see the web page:<br><br>  - val nums1 = 1 :: 2 :: 3 :: []<br>  - val nums2 = 101 :: 102 :: 103 :: []<br>  - val fn1 x y = (2 * x) + y<br>  - foldl fn1 1 nums1 = 13<br>  - foldl fn1 1 nums2 = 613<br>  - mp minus100 nums2 = 1 :: 2 :: 3 :: []<br><br>However, if I uncomment the two lines involving 'eq' and attempt to compile, doing:<br><br>  urweb list_test<br><br>I get the following compile errors:<br><br>  list_test.ur:17:29: (to 17:31) Unification failure<br>  Expression:  eq [<UNIF:U543::Type>] _<br>    Have con:  eq (list <UNIF:U543::Type>)<br>    Need con:  <UNIF:U544::Type> -> <UNIF:U545::Type><br>  Incompatible constructors<br>  Have:  eq (list <UNIF:U543::Type>)<br>  Need:  <UNIF:U544::Type> -> <UNIF:U545::Type><br><br>  list_test.ur:18:43: (to 18:45) Unification failure<br>  Expression:  eq [<UNIF:U628::Type>] _<br>    Have con:  eq (list <UNIF:U628::Type>)<br>    Need con:  <UNIF:U629::Type> -> <UNIF:U630::Type><br>  Incompatible constructors<br>  Have:  eq (list <UNIF:U628::Type>)<br>  Need:  <UNIF:U629::Type> -> <UNIF:U630::Type><br> <br>Questions:<br><br>(1) Have I misunderstood the rank of 'eq'?<br><br>(2) What does 'mkEq' do?<br><br>(3) Why are the signatures for 'eq' in basis.urs and list.urs different?<br><br>I apologize for these sorts of novice questions. I am only somewhat familiar with ML and Haskell, only having read some manuals and tutorials.<br><br>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:<br><br>  <a href="http://cseweb.ucsd.edu/~goguen/pps/utyop.pdf">http://cseweb.ucsd.edu/~goguen/pps/utyop.pdf</a><br><br>- "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.)<br><br>- "higher order logic does not mix well with subsorts"<br><br>- 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)<br><br>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.<br><br>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.<br><br>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!<br><br>###<br><br></span></div></div>