[Ur] exploring folders - I still don't get it.

Mon Apr 16 06:58:36 EDT 2012

Trying to copy paste all the definitions which I think I need to make
the countFields sample from the tutorial work into my own file and
prefixing it by my_ yields this code, and the error shown at the bottom.
Which magic is happening in the standard library I've missed?

Also where exactly is the recursion (repeat until the attribute set has
been processed) happening?
Is it somewhere hidden in the compiler?

Marc Weber

== CODE START ==

  (* using my_ to get different names from top.ur / top.urs *)

  con my_folder = K ==> fn r :: {K} =>
                        tf :: ({K} -> Type)
                        -> (nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
                            tf r -> tf ([nm = v] ++ r))
                        -> tf [] -> tf r

  fun my_fold [K] [tf :: {K} -> Type]
           (f : (nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
                 tf r -> tf ([nm = v] ++ r)))
           (i : tf []) [r ::: {K}] (fl : my_folder r) = fl [tf] f i

  structure Folder = struct
      fun nil [K] [tf :: {K} -> Type]
              (f : nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
               tf r -> tf ([nm = v] ++ r))
              (i : tf []) = i

      fun cons [K] [r ::: {K}] [nm :: Name] [v :: K] [[nm] ~ r] (my_fold : my_folder r)
               [tf :: {K} -> Type]
               (f : nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
                tf r -> tf ([nm = v] ++ r))
               (i : tf []) = f [nm] [v] [r] (my_fold [tf] f i)

      fun concat [K] [r1 ::: {K}] [r2 ::: {K}] [r1 ~ r2]
          (f1 : my_folder r1) (f2 : my_folder r2)
          [tf :: {K} -> Type]
          (f : nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
           tf r -> tf ([nm = v] ++ r))
          (i : tf []) =
          f1 [fn r1' => [r1' ~ r2] => tf (r1' ++ r2)]
             (fn [nm :: Name] [v :: K] [r1' :: {K}] [[nm] ~ r1']
                              (acc : [r1' ~ r2] => tf (r1' ++ r2))
                              [[nm = v] ++ r1' ~ r2] =>
                 f [nm] [v] [r1' ++ r2] acc)
             (fn [[] ~ r2] => f2 [tf] f i)

      fun mp [K1] [K2] [f ::: K1 -> K2] [r ::: {K1}]
          (my_fold : my_folder r)
          [tf :: {K2} -> Type]
          (f : nm :: Name -> v :: K2 -> r :: {K2} -> [[nm] ~ r] =>
           tf r -> tf ([nm = v] ++ r))
          (i : tf []) =
          my_fold [fn r => tf (map f r)]
          (fn [nm :: Name] [v :: K1] [rest :: {K1}] [[nm] ~ rest] (acc : tf (map f rest)) =>
              f [nm] [f v] [map f rest] acc)
          i
  end

  open Folder

  fun countFields [ts :: {Type}] (fl : my_folder ts) : int =
      @my_fold [fn _ => int] (fn [nm ::_] [v ::_] [r ::_] [[nm] ~ r] n => n + 1) 0 fl

  val c:int = countFields [[A = int, B = float, C = string]]

  val main () =
    return <xml>
      <head> <title>Hello world!!</title> </head>
      <body>
        <form>
        {[c]}
        </form>
      </body>
    </xml>
== CODE END ==

  main.ur|59 col 12| 59:58: Unification failure
  || Expression:  countFields [[#A = int, #B = float, #C = string]]
  ||   Have con: 
  || ((tf :: {Type} -> Type ->
  ||    ((nm :: Name ->
  ||       v :: Type ->
  ||        r :: {Type} ->
  ||         [[nm = ()] ~ r] => ((tf r) -> tf (([nm = v]) ++ r))) ->
  ||      ((tf ([])) ->
  ||        tf ([#A = Basis.int, #B = Basis.float, #C = Basis.string]))))
  ||   -> Basis.int)
  ||   Need con:  Basis.int
  || Incompatible constructors
  || Have: 
  || ((tf :: {Type} -> Type ->
  ||    ((nm :: Name ->
  ||       v :: Type ->
  ||        r :: {Type} ->
  ||         [[nm = ()] ~ r] => ((tf r) -> tf (([nm = v]) ++ r))) ->
  ||      ((tf ([])) ->
  ||        tf ([#A = Basis.int, #B = Basis.float, #C = Basis.string]))))
  ||   -> Basis.int)
  || Need:  Basis.int