typeinferencer2.clj

;; # Try 1 - No refreshing

(run* [q]
      (fresh [f f* f** α T1 T2]
        ;; Say we have a polymorphic function f of type ∀α.α → α
        ;; (in Haskell, this would be a -> a).
        (== f [α :-> α])

        ;; Apply it on T1, an Int.
        ;; The type of f in that context is Int → Int.
        (== f f*)
        (== [T1 :-> T1] f*)
        (== T1 :Int)

        ;; Apply it on T2, a Bool.
        ;; The type of f in that context is Bool → Bool.
        (== f f**)
        (== [T2 :-> T2] f**)
        (== T2 :Bool)

        (== [f f* f**] q)))

=> ()
;; No results, as expected because α, T1 and T2 are the same lvar, so
;; it can't be :Int and :Bool at the same time.


;; # Try 2 - With refreshing

(run* [q]
      (fresh [f f* f** α T1 T2]
        ;; Say we have a polymorphic function f of type ∀α.α → α
        ;; (in Haskell, this would be a -> a).
        (== f [α :-> α])

        ;; Apply it on T1, an Int.
        ;; The type of f in that context is Int → Int.
        (refresh f f*)                  ; CHANGED
        (== [T1 :-> T1] f*)
        (== T1 :Int)

        ;; Apply it on T2, a Bool.
        ;; The type of f in that context is Bool → Bool.
        (refresh f f**)                 ; CHANGED
        (== [T2 :-> T2] f**)
        (== T2 :Bool)

        (== [f f* f**] q)))

=> ([[_.0 :-> _.0] [:Int :-> :Int] [:Bool :-> :Bool]])
;; Success! The `refresh` relation replaces all unbound lvars with
;; fresh ones, so α, T1 and T2 are three different lvars. See the
;; bottom of this file for the source of `refresh`.


;; # Try 3 - Too much freshness

(run* [q]
      (fresh [f f* f** α T1 T2]
        ;; Say we have a polymorphic function f of type ∀α.α → Int
        ;; (in Haskell, this would be a -> Int).
        (== f [α :-> :Int])             ; CHANGED

        ;; Apply it on T1, an Int.
        ;; The type of f in that context is Int → Int.
        (refresh f f*)
        (== [T1 :-> T1] f*)
        (== T1 :Int)

        ;; Apply it on T2, a Bool.
        ;; The type of f in that context should be Bool → Bool, but
        ;; the return type of f is already Int, so this should fail.
        (refresh f f**)
        (== [T2 :-> T2] f**)
        (== T2 :Bool)

        (== [f f* f**] q)))

=> ([[_.0 :-> :Int] [:Int :-> :Int] [:Bool :-> :Bool]])
;; It unexpectedly succeeds. We defined f to be [α :-> :Int] so
;; [:Int :-> :Int] is fine, but [:Bool :-> :Bool] should have failed.
;; It appears that the `refresh` function refreshes all lvars
;; (or even the whole expression?)


;; T2 is T1 but with all unground lvars replaced by fresh ones.
;; Example: (fresh [_.0 :-> :Int] [_.1 :-> :Int])
(defn refresh [T1 T2]
  (conda
   ;; If it's an unground lvar, refresh it.
   [(lvaro T1) (fresh [T*] (== T* T2))]
   [(matcha [T1]                       ; I think we never even reach this point!
      ;; Empty list
      ([[]] (== T2 []))
      ;; Walk the car and the cdr
      ([[x . xs]]
         (fresh [x* xs*]
           (refresh x x*)
           (refresh xs xs*)
           (conso x* xs* T2)))
      ;; Just a single constant, not an lvar
      ([x] (== T2 x)))]))

;; While writing this example, I realized another problem:
;; after (fresh [_.0 :-> _.0] T2), T2 should be [_.1 :-> _.1]
;; If `refresh` would do what it currently should do, T2 would be:
;; [_.1 :-> _.2]

;; Short description of the correct implementation refresh
;; (non-relational approach):
;;
;; * Collect a list of all unbound lvars in T1
;; * Zipmap that list with a list of fresh vars
;; * Apply the zipped map as substitutions to T1 to get T2
;;

My Pleasure to write you,
My name is Favor Williams,
My email address is
( [email protected])
Am interested to know
more about you,
Contact me for my
photo and other
important issue via,

[email protected]