User Tools

Site Tools


blog:2010:08:04:typing_haskell_in_ml

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Next revision
Previous revision
blog:2010:08:04:typing_haskell_in_ml [2010/08/04 14:22]
csoldani created
blog:2010:08:04:typing_haskell_in_ml [2011/02/20 20:28] (current)
Line 1: Line 1:
 ====== Typing Haskell in ML ====== ====== Typing Haskell in ML ======
  
-{{tag>​Haskell,OCaml,​Programming}}+{{tag>Compiler ​Haskell OCaml}}
  
 This post presents a quick translation of the haskell code of the article [[http://​web.cecs.pdx.edu/​~mpj/​thih/​|Typing Haskell in Haskell]] by Mark P. Jones to OCaml. This post presents a quick translation of the haskell code of the article [[http://​web.cecs.pdx.edu/​~mpj/​thih/​|Typing Haskell in Haskell]] by Mark P. Jones to OCaml.
Line 30: Line 30:
 The type inference monad has been replaced by mutable state which is passed explicitely such that a function which had the haskell type The type inference monad has been replaced by mutable state which is passed explicitely such that a function which had the haskell type
 <code haskell> <code haskell>
-f :: -> TI b+f :: SomeType ​-> TI OtherType
 </​code>​ </​code>​
 has the OCaml type has the OCaml type
 <code ocaml> <code ocaml>
-val f : ti -> -> b+val f : ti -> someType ​-> otherType
 </​code>​ </​code>​
  
 ===== The Code ===== ===== The Code =====
  
-<file ocaml typingHaskellInML.ml>​ +{{:blog:2010:08:​04:​typinghaskellinml.ml}}
-(* +
- * This file is a translation of the code pertaining to the article +
- * `Typing Haskell in Haskell'​ by Mark P. Jones [1], from Haskell to OCaml. +
- * +
- * 1http://​web.cecs.pdx.edu/​~mpj/​thih/​ +
- * +
- * Copyright (C) 1999 - 2000  Mark P. Jones +
- * Copyright (C) 2010 Cyril Soldani +
- * +
- * Here follows the license (license of the original Haskell code from the +
- * article). +
- * +
- * `Typing Haskell in Haskell'​ is Copyright (c) Mark P Jones +
- * and the Oregon Graduate Institute of Science and Technology,​ +
- * 1999-2000, All rights reserved, and is distributed as +
- * free software under the following license. +
- * +
- * Redistribution and use in source and binary forms, with or +
- * without modification,​ are permitted provided that the following +
- * conditions are met: +
- * +
- * - Redistributions of source code must retain the above copyright +
- * notice, this list of conditions and the following disclaimer. +
- * +
- * - Redistributions in binary form must reproduce the above +
- * copyright notice, this list of conditions and the following +
- * disclaimer in the documentation and/or other materials provided +
- * with the distribution. +
- * +
- * - Neither name of the copyright holders nor the names of its +
- * contributors may be used to endorse or promote products derived +
- * from this software without specific prior written permission. +
- * +
- * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND THE +
- * CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES,​ +
- * INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF +
- * MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +
- * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR THE +
- * CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,​ +
- * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT +
- * NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +
- * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +
- * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, +
- * STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) +
- * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF +
- * ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +
- *)+
  
-open Big_int +~~DISCUSSION~~ ​
-open List +
-open Num +
- +
-(* 2 Preliminaries *) +
- +
-let union xs ys = filter (fun x -> not (mem x ys)) xs @ ys +
- +
-let intersect xs ys = filter (fun x -> mem x ys) xs +
- +
-let nub xs = +
-   let addToSet ys y = if mem y ys then ys else y :: ys in +
-   ​fold_left addToSet [] xs +
- +
-let isEmpty = function +
-     [] -> true +
-   | _ -> false +
- +
-let fold_left1 f = function +
-     [] -> invalid_arg "empty list"​ +
-   | [x] -> x +
-   | x :: xs -> fold_left f x xs +
- +
-let rec deleteFirst x = function +
-     [] -> [] +
-   | y :: ys -> +
-        if x = y then ys +
-        else y :: deleteFirst x ys +
- +
-let rec diff xs = function +
-     [] -> xs +
-   | y :: ys -> diff (deleteFirst y xs) ys +
- +
-let split3 xs = +
-   let rec loop (ws, xs, ys) = function +
-        [] -> (rev ws, rev xs, rev ys) +
-      | (w, x, y) :: zs -> loop (w :: ws, x :: xs, y :: ys) zs in +
-   loop ([], [], []) xs +
- +
-type id = string +
- +
-let enumId n : id = "​v"​ ^ string_of_int n +
- +
-(* 3 Kinds *) +
- +
-type kind = Star | Kfun of kind * kind +
- +
-(* 4 Types *) +
- +
-type tyvar = Tyvar of id * kind +
-type tycon = Tycon of id * kind +
-type type_ = TVar of tyvar | TCon of tycon | TAp of type_ * type_ | TGen of int +
- +
-let tUnit = TCon(Tycon("​()",​ Star)) +
-let tChar = TCon(Tycon("​Char",​ Star)) +
-let tInt = TCon(Tycon("​Int",​ Star)) +
-let tInteger = TCon(Tycon("​Integer",​ Star)) +
-let tFloat = TCon(Tycon("​Float",​ Star)) +
-let tDouble = TCon(Tycon("​Double",​ Star)) +
- +
-let tList = TCon(Tycon("​[]",​ Kfun(Star, Star))) +
-let tArrow = TCon(Tycon("​(->​)",​ Kfun(Star, Kfun(Star, Star)))) +
-let tTuple2 = TCon(Tycon("​(,​)",​ Kfun(Star, Kfun(Star, Star)))) +
- +
-let fn a b = TAp(TAp(tArrow,​ a), b) +
- +
-let list t = TAp(tList, t) +
- +
-let tString = list tChar +
- +
-let pair a b = TAp(TAp(tTuple2,​ a), b) +
- +
-let tyvarKind (Tyvar(_, k)) = k +
-let tyconKind (Tycon(_, k)) = k +
-let rec typeKind = function +
-     TCon tc -> tyconKind tc +
-   | TVar u -> tyvarKind u +
-   | TAp(t, _) -> +
-        begin match typeKind t with +
-             ​Kfun(_,​ k) -> k +
-           | _ -> failwith "​inconsistent type"​ +
-        end +
-   | TGen _ -> failwith "​generic type variables have no kind"​ +
- +
-(* 5 Substitutions *) +
- +
-type subst = (tyvar * type_) list +
- +
-let nullSubst : subst = [] +
- +
-let (+->) u t : subst = [(u, t)] +
- +
-let rec typeApply (s : subst) = function +
-     TVar u as t -> +
-        begin try assoc u s +
-        with Not_found -> t +
-        end +
-   | TAp(l, r) -> TAp(typeApply s l, typeApply s r) +
-   | t -> t +
- +
-let rec typeTv = function +
-     TVar u -> [u] +
-   | TAp(l, r) -> union (typeTv l) (typeTv r) +
-   | _ -> [] +
- +
-let listApply (apply : subst -> 'a -> 'a) (s : subst) xs = map (apply s) xs +
-let listTv tv xs : tyvar list = nub (concat (map tv xs)) +
- +
-let (@@) s1 (s2 : subst) : subst = +
-   map (fun (u, t) -> (u, typeApply s1 t)) s2 @ s1 +
- +
-let merge s1 s2 : subst = +
-   let agree = +
-      let agreeOnVar v = typeApply s1 (TVar v) = typeApply s2 (TVar v) in +
-      for_all agreeOnVar (intersect (map fst s1) (map fst s2)) in +
-   if agree then s1 @ s2 else failwith "​substitutions do not agree"​ +
- +
-(* 6 Unification and Matching *) +
- +
-let rec mgu t1 t2 = +
-   match t1, t2 with +
-        TAp(l, r), TAp(l',​ r') -> +
-           let s1 = mgu l l' in +
-           let s2 = mgu (typeApply s1 r) (typeApply s1 r') in +
-           s2 @@ s1 +
-      | TVar u, t | t, TVar u -> varBind u t +
-      | TCon tc1, TCon tc2 when tc1 = tc2 -> nullSubst +
-      | _ -> failwith "types do not unify"​ +
-and varBind u t = +
-   if t = TVar u then nullSubst +
-   else if mem u (typeTv t) then failwith "​occurs check fails"​ +
-   else if tyvarKind u <> typeKind t then failwith "kinds do not match"​ +
-   else u +-> t +
- +
-let rec match_ t1 t2 = +
-   match t1, t2 with +
-        TAp(l, r), TAp(l',​ r') -> +
-           let sl = match_ l l' in +
-           let sr = match_ r r' in +
-           merge sl sr +
-      | TVar u, t when tyvarKind u = typeKind t -> u +-> t +
-      | TCon tc1, TCon tc2 when tc1 = tc2 -> nullSubst +
-      | _ -> failwith "types do not match"​ +
- +
-(* 7 Type Classes, Predicates and Qualified Types *) +
- +
-(* 7.1 Basic definitions *) +
- +
-type pred = IsIn of id * type_ +
-type 't qual = Qual of pred list * 't +
- +
-let predApply s (IsIn(i, t)) = IsIn(i, typeApply s t) +
-let predsApply = listApply predApply +
- +
-let qualTypeApply s (Qual(ps, t)) = Qual(predsApply s ps, typeApply s t) +
- +
-let predTv (IsIn(_, t)) = typeTv t +
-let predsTv = listTv predTv +
- +
-let qualTypeTv (Qual(ps, t)) = union (predsTv ps) (typeTv t) +
- +
-let lift m (IsIn(i, t)) (IsIn(i',​ t')) = +
-   if i = i' then m t t' +
-   else failwith "​classes differ"​ +
- +
-let mguPred = lift mgu +
-let matchPred = lift match_ +
- +
-type inst = pred qual +
-type class_ = id list * inst list +
- +
-(* 7.2 Class Environments *) +
- +
-type classEnv = { +
-   ​classes : (id -> class_); +
-   ​defaults : type_ list; +
-+
- +
-let super ce i = fst (ce.classes i) +
- +
-let insts ce i = snd (ce.classes i) +
- +
-let defined ce i = +
-   try +
-      ignore (ce.classes i); +
-      true +
-   with Not_found -> false +
- +
-let modify ce i c = +
-   { ce with classes = fun j -> if i = j then c else ce.classes j; } +
- +
-let initalEnv = { +
-   ​classes = (fun i -> raise Not_found);​ +
-   ​defaults = [tInteger; tDouble] +
-+
- +
-type envTransformer = classEnv -> classEnv +
- +
-let (<:>) (f : envTransformer) (g : envTransformer) : envTransformer = +
-   fun ce -> g (f ce) +
- +
-let addClass i is : envTransformer = +
-   fun ce -> +
-      if defined ce i then failwith "class already defined"​ +
-      else if exists (fun i -> not (defined ce i)) is then +
-         ​failwith "​superclass not defined"​ +
-      else modify ce i (is, []) +
- +
-let addCoreClasses = +
-       ​addClass "​Eq"​ [] +
-   <:>​ addClass "​Ord"​ ["​Eq"​] +
-   <:>​ addClass "​Show"​ [] +
-   <:>​ addClass "​Read"​ [] +
-   <:>​ addClass "​Bounded"​ [] +
-   <:>​ addClass "​Enum"​ [] +
-   <:>​ addClass "​Functor"​ [] +
-   <:>​ addClass "​Monad"​ [] +
- +
-let addNumClasses = +
-       ​addClass "​Num"​ ["​Eq";​ "​Show"​] +
-   <:>​ addClass "​Real"​ ["​Num";​ "​Ord"​] +
-   <:>​ addClass "​Fractional"​ ["​Num"​] +
-   <:>​ addClass "​Integral"​ ["​Real";​ "​Enum"​] +
-   <:>​ addClass "​RealFrac"​ ["​Real";​ "​Fractional"​] +
-   <:>​ addClass "​Floating"​ ["​Fractional"​] +
-   <:>​ addClass "​RealFloat"​ ["​RealFrac";​ "​Floating"​] +
- +
-let addPreludeClasses = addCoreClasses <:> addNumClasses +
- +
-let overlap p q = +
-   try +
-      ignore (mguPred p q); +
-      true +
-   with _ -> false +
- +
-let addInst ps (IsIn(i, _) as p) : envTransformer = +
-   fun ce -> +
-      if not (defined ce i) then failwith "no class for instance"​ +
-      else +
-         let its = insts ce i in +
-         let qs = map (fun (Qual(_, q)) -> q) its in +
-         if exists (overlap p) qs then failwith "​overlapping instance"​ +
-         ​else +
-            let c = super ce i, Qual(ps, p) :: its in +
-            modify ce i c +
- +
-let exampleInsts = +
-       ​addPreludeClasses +
-   <:>​ addInst [] (IsIn("​Ord",​ tUnit)) +
-   <:>​ addInst [] (IsIn("​Ord",​ tChar)) +
-   <:>​ addInst [] (IsIn("​Ord",​ tInt)) +
-   <:>​ addInst [IsIn("​Ord",​ TVar(Tyvar("​a",​ Star))); +
-                IsIn("​Ord",​ TVar(Tyvar("​b",​ Star)))] +
-               ​(IsIn("​Ord",​ pair (TVar(Tyvar("​a",​ Star))) +
-                                 ​(TVar(Tyvar("​b",​ Star))))) +
- +
-(* 7.3 Entailment *) +
- +
-let rec bySuper ce (IsIn(i, t) as p) = +
-   p :: concat (map (fun i' -> bySuper ce (IsIn(i',​ t))) (super ce i)) +
- +
-let byInst ce (IsIn(i, t) as p) = +
-   let tryInst (Qual(ps, h)) = +
-      let u = matchPred h p in +
-      map (predApply u) ps in +
-   ​concat (map tryInst (insts ce i)) +
- +
-let rec entail ce ps p = +
-   ​exists (mem p) (map (bySuper ce) ps) || +
-   try for_all (entail ce ps) (byInst ce p) +
-   with _ -> false +
- +
-(* 7.4 Context Reduction *) +
- +
-let inHnf (IsIn(_, t)) = +
-   let rec hnf = function +
-        TVar _ -> true +
-      | TCon _ -> false +
-      | TAp(t, _) -> hnf t +
-      | TGen _ -> failwith "​context reduction on generic variable"​ in +
-   hnf t +
- +
-let rec toHnfs ce ps = concat (map (toHnf ce) ps) +
-and toHnf ce p = +
-   if inHnf p then [p] +
-   ​else +
-      try toHnfs ce (byInst ce p) +
-      with _ -> failwith "​context reduction"​ +
- +
-let simplify ce ps = +
-   let rec loop rs = function +
-        [] -> rs +
-      | p :: ps -> +
-           if entail ce (rs @ ps) p then loop rs ps +
-           else loop (p :: rs) ps in +
-   loop [] ps +
- +
-let reduce ce ps = simplify ce (toHnfs ce ps) +
- +
-let scEntail ce ps p = exists (mem p) (map (bySuper ce) ps) +
- +
-(* 8 Type Schemes *) +
- +
-type scheme = Forall of kind list * type_ qual +
- +
-let schemeApply s (Forall(ks, qt)) = Forall(ks, qualTypeApply s qt) +
- +
-let schemeTv (Forall(_, qt)) = qualTypeTv qt +
- +
-let quantify vs qt = +
-   let vs' = filter (fun v -> mem v vs) (qualTypeTv qt) in +
-   let ks = map tyvarKind vs' in +
-   let newGen v = +
-      let count = ref 0 in +
-      let t = TGen !count in +
-      incr count; +
-      (v, t) in +
-   let s = map newGen vs' in +
-   ​Forall(ks,​ qualTypeApply s qt) +
- +
-let toScheme t = Forall([], (Qual([], t))) +
- +
-(* 9 Assumptions *) +
- +
-type assump = Assump of id * scheme +
- +
-let assumpApply s (Assump(i, sc)) = Assump(i, schemeApply s sc) +
- +
-let assumpTv (Assump(_, sc)) = schemeTv sc +
- +
-let assumpsApply = listApply assumpApply +
- +
-let assumpsTv = listTv assumpTv +
- +
-let find i as_ = +
-   let Assump(_, sc) = List.find (fun (Assump(i',​ _)) -> i = i') as_ in +
-   sc +
- +
-(* 10 A Type Inference Monad *) +
- +
-type ti = subst ref * int ref +
- +
-let runTI (f : ti -> 'a) = f (ref nullSubst, ref 0) +
- +
-let getSubst ((s, _) : ti) = !s +
- +
-let extSubst ((s, _) : ti) u = s := u @@ !s +
- +
-let unify ti t1 t2 = +
-   let s = getSubst ti in +
-   let u = mgu (typeApply s t1) (typeApply s t2) in +
-   ​extSubst ti u +
- +
-let newTVar ((_, n) : ti) k = +
-   let v = Tyvar(enumId !n, k) in +
-   incr n; +
-   TVar v +
- +
-let rec typeInst ts = function +
-     ​TAp(l,​ r) -> TAp(typeInst ts l, typeInst ts r) +
-   | TGen n -> nth ts n +
-   | t -> t +
- +
-let listInst inst (ts : type_ list) (xs : 'a list) : 'a list = map (inst ts) xs +
- +
-let predInst ts (IsIn(c, t)) = IsIn(c, typeInst ts t) +
- +
-let qualTypeInst ts (Qual(ps, t)) = Qual(listInst predInst ts ps, typeInst ts t) +
- +
-let freshInst ti (Forall(ks, qt)) = +
-   let ts = map (newTVar ti) ks in +
-   ​qualTypeInst ts qt +
- +
-(* 11 Type Inference *) +
- +
-type ('e, 't) infer = ti -> classEnv -> assump list -> 'e -> pred list * 't +
- +
-(* 11.1 Literals *) +
- +
-type literal = +
-     ​LitInt of big_int +
-   | LitChar of char +
-   | LitRat of num +
-   | LitStr of string +
- +
-let tiLit ti = function +
-     ​LitChar _ -> ([], tChar) +
-   | LitInt _ -> +
-        let v = newTVar ti Star in +
-        ([IsIn("​Num",​ v)], v) +
-   | LitStr _ -> ([], tString) +
-   | LitRat _ -> +
-        let v = newTVar ti Star in +
-        ([IsIn("​Fractional",​ v)], v) +
- +
-(* 11.2 Patterns *) +
- +
-type pat = +
-     PVar of id +
-   | PWildcard +
-   | PAs of id * pat +
-   | PLit of literal +
-   | PNpk of id * big_int +
-   | PCon of assump * pat list +
- +
-let rec tiPat ti = function +
-     PVar i -> +
-        let t = newTVar ti Star in +
-        ([], [Assump(i, toScheme t)], t) +
-   | PWildcard -> ([], [], newTVar ti Star) +
-   | PAs(i, pat) -> +
-        let (ps, as_, t) = tiPat ti pat in +
-        (ps, Assump(i, toScheme t) :: as_, t) +
-   | PLit l -> +
-        let (ps, t) = tiLit ti l in +
-        (ps, [], t) +
-   | PNpk(i, k) -> +
-        let t = newTVar ti Star in +
-        ([IsIn("​Integral",​ t)], [Assump(i, toScheme t)], t) +
-   | PCon(Assump(i,​ sc), pats) -> +
-        let (ps, as_, ts) = tiPats ti pats in +
-        let t' = newTVar ti Star in +
-        let Qual(qs, t) = freshInst ti sc in +
-        unify ti t (fold_right fn ts t'); +
-        (ps @ qs, as_, t') +
-and tiPats ti pats = +
-   let (pss, ass, ts) = split3 (map (tiPat ti) pats) in +
-   ​(concat pss, concat ass, ts) +
- +
-(* 11.3 Expressions +
- * 11.4 Alternatives +
- * 11.5 From Types to Type Schemes +
- * 11.6 Binding Groups *) +
- +
-type ambiguity = tyvar * pred list +
- +
-let ambiguities vs ps : ambiguity list = +
-   let vs' = diff (predsTv ps) vs in +
-   map (fun v -> (v, filter (fun p -> mem v (predTv p)) ps)) vs' +
- +
-let numClasses : id list = [ +
-   "​Num";​ "​Integral";​ "​Floating";​ "​Fractional";​ "​Real";​ "​RealFloat";​ +
-   "​RealFrac"​] +
- +
-let stdClasses : id list = [ +
-   "​Eq";​ "​Ord";​ "​Show";​ "​Read";​ "​Bounded";​ "​Enum";​ "​Ix";​ "​Functor";​ "​Monad";​ +
-   "​MonadPlus"​] @ numClasses +
- +
-let candidates ce ((v, qs) : ambiguity) = +
-   let is = map (fun (IsIn(i, _)) -> i) qs in +
-   let ts = map (fun (IsIn(_, t)) -> t) qs in +
-   if for_all (fun t -> t = TVar v) ts &&​ +
-      exists (fun i -> mem i numClasses) is &&​ +
-      for_all (fun i -> mem i stdClasses) is then +
-      let isCandidate t' = +
-         ​for_all (entail ce []) (map (fun i -> IsIn(i, t')) is) in +
-      filter isCandidate ce.defaults +
-   else [] +
- +
-let withDefaults f ce vs ps = +
-   let vps = ambiguities vs ps in +
-   let tss = map (candidates ce) vps in +
-   if exists isEmpty tss then failwith "​cannot resolve ambiguity"​ +
-   else f vps (map hd tss) +
- +
-let defaultedPreds = withDefaults (fun vps ts -> concat (map snd vps)) +
- +
-let defaultSubst ce vs ps : subst = +
-   ​withDefaults (fun vps ts -> combine (map fst vps) ts) ce vs ps +
- +
-let split ce fs gs ps = +
-   let ps' = reduce ce ps in +
-   let (ds, rs) = +
-      partition (fun p -> for_all (fun t -> mem t fs) (predTv p)) ps' in +
-   let rs' = defaultedPreds ce (fs @ gs) rs in +
-   (ds, diff rs rs') +
- +
-type alt = pat list * expr +
-and expl = id * scheme * alt list +
-and impl = id * alt list +
-and bindGroup = expl list * impl list list +
-and expr = +
-     Var of id +
-   | Lit of literal +
-   | Const of assump +
-   | Ap of expr * expr +
-   | Let of bindGroup * expr +
- +
-let restricted (bs : impl list) = +
-   let simple (i, alts) = exists (fun alt -> isEmpty (fst alt)) alts in +
-   ​exists simple bs +
- +
-let rec tiSeq (f : ('bg, assump list) infer) : ('bg list, assump list) infer = +
-   fun ti ce as_ -> function +
-        [] -> ([], []) +
-      | bs :: bss -> +
-           let (ps, as') = f ti ce as_ bs in +
-           let (qs, as''​) = tiSeq f ti ce (as' @ as_) bss in +
-           (ps @ qs, as''​ @ as') +
- +
-let rec tiExpr ti ce as_ = function +
-     Var i -> +
-        let sc = find i as_ in +
-        let Qual(ps, t) = freshInst ti sc in +
-        (ps, t) +
-   | Const(Assump(_,​ sc)) -> +
-        let Qual(ps, t) = freshInst ti sc in +
-        (ps, t) +
-   | Lit l -> tiLit ti l +
-   | Ap(e, f) -> +
-        let (ps, te) = tiExpr ti ce as_ e in +
-        let (qs, tf) = tiExpr ti ce as_ f in +
-        let t = newTVar ti Star in +
-        unify ti (fn tf t) te; +
-        (ps @ qs, t) +
-   | Let(bg, e) -> +
-        let (ps, as') = tiBindGroup ti ce as_ bg in +
-        let (qs, t) = tiExpr ti ce (as' @ as_) e in +
-        (ps @ qs, t) +
-and tiAlt : (alt, type_) infer = +
-   fun ti ce as_ (pats, e) -> +
-      let (ps, as', ts) = tiPats ti pats in +
-      let (qs, t) = tiExpr ti ce (as' @ as_) e in +
-      (ps @ qs, fold_right fn ts t) +
-and tiAlts ti ce as_ alts t = +
-   let (ps, ts) = List.split (map (tiAlt ti ce as_) alts) in +
-   iter (unify ti t) ts; +
-   ​concat ps +
-and tiExpl ti ce as_ ((i, sc, alts) : expl) = +
-   let Qual(qs, t) = freshInst ti sc in +
-   let ps = tiAlts ti ce as_ alts t in +
-   let s = getSubst ti in +
-   let qs' = predsApply s qs in +
-   let t' = typeApply s t in +
-   let fs = assumpsTv (assumpsApply s as_) in +
-   let gs = diff (typeTv t') fs in +
-   let sc' = quantify gs (Qual(qs',​ t')) in +
-   let ps' = filter (fun p -> not (entail ce qs' p)) (predsApply s ps) in +
-   let (ds, rs) = split ce fs gs ps' in +
-   if sc <> sc' then failwith "​signature too general"​ +
-   else if not (isEmpty rs) then failwith "​context too weak"​ +
-   else ds +
-and tiImpls : (impl list, assump list) infer = +
-   fun ti ce as_ bs -> +
-      let ts = map (fun _ -> newTVar ti Star) bs in +
-      let (is, altss) = List.split bs in +
-      let scs = map toScheme ts in +
-      let as' = map2 (fun i sc -> Assump(i, sc)) is scs @ as_ in +
-      let pss = map2 (tiAlts ti ce as') altss ts in +
-      let s = getSubst ti in +
-      let ps' = map (predApply s) (concat pss) in +
-      let ts' = map (typeApply s) ts in +
-      let fs = assumpsTv (assumpsApply s as_) in +
-      let vss = map typeTv ts' in +
-      let gs = diff (fold_left1 union vss) fs in +
-      let (ds, rs) = split ce fs (fold_left1 intersect vss) ps' in +
-      if restricted bs then +
-         let gs' = diff gs (predsTv rs) in +
-         let scs' = map (fun t -> quantify gs' (Qual([], t))) ts' in +
-         (ds @ rs, map2 (fun i sc -> Assump(i, sc)) is scs'​) +
-         ​else +
-            let scs' = map (fun t -> quantify gs (Qual(rs, t))) ts' in +
-            (ds, map2 (fun i sc -> Assump(i, sc)) is scs'​) +
-and tiBindGroup : (bindGroup, assump list) infer = +
-   fun ti ce as_ (es, iss) -> +
-      let as' = map (fun (v, sc, _) -> Assump(v, sc)) es in +
-      let (ps, as''​) = tiSeq tiImpls ti ce (as' @ as_) iss in +
-      let qss = map (tiExpl ti ce (as''​ @ as' @ as_)) es in +
-      (ps @ concat qss, as''​ @ as') +
- +
-type program = bindGroup list +
- +
-let tiProgram ce as_ (bgs : program) = +
-   runTI (fun ti -> +
-             let (ps, as') = tiSeq tiBindGroup ti ce as_ bgs in +
-             let s = getSubst ti in +
-             let rs = reduce ce (predsApply s ps) in +
-             let s' = defaultSubst ce [] rs in +
-             ​assumpsApply (s' @@ s) as') +
-</​file>​ +
- +
-~~DISCUSSION~~+
blog/2010/08/04/typing_haskell_in_ml.1280924575.txt.gz · Last modified: 2011/02/20 20:28 (external edit)