progress on self-hosting

Today the self-hosted Irken compiled its first complete program, all the way through substituting into the header template file, and compiling via gcc. A nice feeling.

;; -*- Mode: Irken -*-

(datatype list
  (:nil)
  (:cons 'a (list 'a))
  )

(defmacro list
  (list)         -> (list:nil)
  (list x y ...) -> (list:cons x (list y ...)))

(define (+ a b)
  (%%cexp (int int -> int) "%0+%1" a b))

(define length
  () -> 0
  (_ . tl) -> (+ 1 (length tl)))

(length (list 1 2 3))

I also finally got around to checking in the changes from the last couple of weeks, too much slacking off there.

Y combinator in Irken

The second version requires recursive types.

;; -*- Mode: Irken -*-

;; See http://en.wikipedia.org/wiki/Fixed_point_combinator

(include "lib/core.scm")

(define (Y f)
  (lambda (x)
    ((f (Y f)) x)))

(define (factabs fact)
  (lambda (x)
    (if (= x 0)
        1
        (* x (fact (- x 1))))))

(printn ((Y factabs) 5))

;; and http://caml.inria.fr/pub/docs/u3-ocaml/ocaml-ml.html#toc5
;; let fix f' = let g f x = f' (f f) x in (g g);;
;; let fact = fix fact' in fact 5;;

(define (Y2 f1)
  ;; the '^' prefix tells the compiler not to inline this function
  ;;  which in this particular case would never terminate...
  (define (^g f)
    (lambda (x)
      (f1 (f f) x)))
  (^g ^g))

(define (fact1 fact x)
  (if (= x 0)
      1
      (* x (fact (- x 1)))))

(printn ((Y2 fact1) 5))

The function ^g has type

μ(A, (A->b))->(c->d)

recursive types, unification, sharing

I'm having trouble with recursive types in my type reconstruction (type inference) algorithm, some kind of combinatorial explosion.  I think there are multiple triggers for this: at each call to unify(), I'm running a complete apply-subst(), rather than a level at a time.  For the massive types generated by my OO code, this means lots of wasted, repeated work.

But of course there's even more going on.  I think my code that detects recursive types is not working as well as it should, and I think the cause is the lack of 'sharing'.  Remy/Pottier use a different style of unification, that involves preserving shared elements of types, and I think this where I'm screwing up: because parts of types are being copied, I'm missing links between identical parts of the graph.

I found a nice presentation from Remy describing "Core ML", that explains this in (accented) English, rather than a relentless flurry of LaTeX: "Using, Understanding, and Unraveling The OCaml Language: From Practice to Theory and vice versa".

The constraint-oriented solver gave me recursive types for free, (because its output types are naturally graphs), but I'm really hoping to avoid going back to that code, because it's much slower and I frankly don't understand it as well as I'd like.  Maybe I can pull out just the multi-equation unification stuff, and get back recursive types.