// Learn more about F# at http://fsharp.net
// Hindley Milner Type Inference Sample Implementation
// ************************************************
// AST
// ************************************************
type Literal
= Char of char // character literal
| String of string // string literal
| Integer of int // integer literal
| Float of float // floating point literal
type Exp
= Var of string // variable
| Lam of string * Exp // lambda abstraction
| App of Exp * Exp // application
| InfixApp of Exp * string * Exp // infix application
| Let of string * Exp * Exp // local definition
| Lit of Literal // literal
// ************************************************
// Type Tree
// ************************************************
type Type
= TyLam of Type * Type
| TyVar of string
| TyCon of string * Type list
with override this.ToString() =
match this with
| TyLam (t1, t2) -> sprintf "(%s -> %s)" (t1.ToString()) (t2.ToString())
| TyVar a -> a
| TyCon (s, ts) -> s
// ************************************************
// Subtitutions
// ************************************************
type Subst = Subst of Map<string, Type>
// extend: string -> Type -> Subst -> Subst
let extend v t (Subst s) = Subst (Map.add v t s)
// lookup: string -> Subst -> Type
let lookup v (Subst s) =
if (Map.containsKey v s) then
Map.find v s
else
TyVar v
// Apply a type substitution to a type
// subs: Type -> Subst -> Type
let rec subs t s =
match t with
| TyVar n ->
let t' = lookup n s
if t = t' then t'
else subs t' s
| TyLam(a, r) ->
TyLam(subs a s, subs r s)
| TyCon(name, tyArgs) ->
TyCon(name, tyArgs
|> List.map (fun x -> subs x s))
// ************************************************
// Environments
// ************************************************
type TyScheme = TyScheme of Type * Set<string>
type Env = Env of Map<string, TyScheme>
// Calculate the list of type variables occurring in a type,
// without repeats
// getTVarsOfType: Type -> Set<string>
let rec getTVarsOfType t =
match t with
| TyVar n -> Set.singleton n
| TyLam(t1, t2) -> getTVarsOfType(t1) + getTVarsOfType(t2)
| TyCon(_, args) ->
List.fold (fun acc t -> acc + getTVarsOfType t) Set.empty args
// getTVarsOfScheme: TyScheme -> Set<string>
let getTVarsOfScheme (TyScheme (t, tvars)) =
(getTVarsOfType t) - tvars
// getTVarsOfEnv: Env -> Set<string>
let getTVarsOfEnv (Env e) =
let schemes = e |> Map.toSeq |> Seq.map snd
Seq.fold (fun acc s -> acc + (getTVarsOfScheme s)) Set.empty schemes
// ************************************************************
// Unification
// ************************************************************
exception UnificationError of Type * Type
// Calculate the most general unifier of two types,
// raising a UnificationError if there isn't one
// mgu: Type -> Type -> Subst -> Subst
let rec mgu a b s =
match (subs a s, subs b s) with
| TyVar ta, TyVar tb when ta = tb -> s
| TyVar ta, _ when not <| Set.contains ta (getTVarsOfType b) -> extend ta b s
| _, TyVar _ -> mgu b a s
| TyLam (a1, b1), TyLam (a2, b2) -> mgu a1 a2 (mgu b1 b2 s)
| TyCon(name1, args1), TyCon(name2, args2) when name1 = name2 ->
(s, args1, args2) |||> List.fold2 (fun subst t1 t2 -> mgu t1 t2 subst)
| x,y -> raise <| UnificationError (x,y)
// ************************************************************
// State Monad
// ************************************************************
type State<'state, 'a> = State of ('state ->'a * 'state)
let run (State f) s = f s
type StateMonad() =
member b.Bind(State m, f) =
State (fun s ->
let (v,s') = m s in
let (State n) = f v in n s')
member b.Return x = State (fun s -> x, s)
member b.ReturnFrom x = x
member b.Zero () = State (fun s -> (), s)
member b.Combine(r1, r2) = b.Bind(r1, fun () -> r2)
member b.Delay f = State (fun s -> run (f()) s)
let state = StateMonad()
let getState = State (fun s -> s, s)
let setState s = State (fun _ -> (), s)
let execute m s = match m with
| State f -> let r = f s
match r with
|(x,_) -> x
let mmap f xs =
let rec MMap' (f, xs', out) =
state { match xs' with
| h :: t ->
let! h' = f(h)
return! MMap'(f, t, List.append out [h'])
| [] -> return out }
MMap' (f, xs, [])
// ************************************************************
// Alpha converter (Converts T4, T5, T6 to 'a, 'b, 'c)
// ************************************************************
let getName k =
let containsKey k = state { let! (map, id) = getState
return Map.containsKey k map }
let addName k = state { let! (map, id) = getState
let newid = char (int id + 1)
do! setState(Map.add k id map, newid)
return () }
state { let! success = containsKey k
if (not success) then
do! addName k
let! (map, id) = getState
return Map.find k map }
// renameTVarsToLetters: Type -> Type
let renameTVarsToLetters t =
let rec run x =
state {
match x with
| TyVar(name) ->
let! newName = getName name
return TyVar(sprintf "'%c" newName)
| TyLam(arg, res) ->
let! t1 = run arg
let! t2 = run res
return TyLam(t1, t2)
| TyCon(name, typeArgs) ->
let! list = mmap (fun x -> run x) typeArgs
return TyCon(name, list) }
execute (run t) (Map.empty, 'a')
// ****************************************************************
// Calculate principal Type
// ****************************************************************
let newTyVar =
state { let! x = getState
do! setState(x + 1)
return TyVar(sprintf "T%d" x) }
let integerCon = TyCon("int", [])
let floatCon = TyCon("float", [])
let charCon = TyCon("char", [])
let stringCon = TyCon("string", [])
let litToTy lit =
match lit with
| Integer _ -> integerCon
| Float _ -> floatCon
| Char _ -> charCon
| String _ -> stringCon
// Calculate the principal type scheme for an expression in a given
// typing environment
// tp: Env -> Exp -> Type -> Subst -> State<int, Subst>
let rec tp env exp bt s =
let findSc n (Env e) = Map.find n e
let containsSc n (Env e) = Map.containsKey n e
let addSc n sc (Env e) = Env (Map.add n sc e)
state {
match exp with
| Lit v ->
return mgu (litToTy v) bt s
| Var n ->
if not (containsSc n env)
then failwith "Name %s no found" n
let (TyScheme (t, _)) = findSc n env
return mgu (subs t s) bt s
| Lam (x, e) ->
let! a = newTyVar
let! b = newTyVar
let s1 = mgu bt (TyLam (a, b)) s
let newEnv = addSc x (TyScheme (a, Set.empty)) env
return! tp newEnv e b s1
| App(e1, e2) ->
let! a = newTyVar
let! s1 = tp env e1 (TyLam(a, bt)) s
return! tp env e2 a s1
| InfixApp(e1, op, e2) ->
let exp1 = App(App(Var op, e1), e2)
return! tp env exp1 bt s
| Let(name, inV, body) ->
let! a = newTyVar
let! s1 = tp env inV a s
let t = subs a s1
let newScheme = TyScheme (t, ((getTVarsOfType t) - (getTVarsOfEnv env)))
return! tp (addSc name newScheme env) body bt s1 }
let predefinedEnv =
Env(["+", TyScheme (TyLam(integerCon, TyLam(integerCon, integerCon)), Set.empty)
"*", TyScheme (TyLam(integerCon, TyLam(integerCon, integerCon)), Set.empty)
"-", TyScheme (TyLam(integerCon, TyLam(integerCon, integerCon)), Set.empty)
] |> Map.ofList)
// typeOf: Exp -> Type
let typeOf exp =
let typeOf' exp =
state { let! (a:Type) = newTyVar
let emptySubst = Subst (Map.empty)
let! s1 = tp predefinedEnv exp a emptySubst
return subs a s1 }
in execute (typeOf' exp) 0 |> renameTVarsToLetters
// ***********************************************************
// Example
// ***********************************************************
let composeAst = Let("compose",
Lam("f",
Lam("g",
Lam ("x",
App(Var "g", App(Var "f", Var "x"))))),
Var "compose")
let t = typeOf composeAst
printfn "%s" (t.ToString())
2 comments:
Great fun, and more fun is that I have programmed something very much along the same lines. I have found that the following two functions are great to use:
let mapState f = State(fun s-> (), f s)
let foldState f = State (fun s -> f s)
Having defined operators on the "environement" that is carried by the state monad, these two operators can be used to convert them into state monad compatible form. For example, having newVar: Env -> (Type, Env), then I can write:
let newVar' = foldState newVar and in the computation expression write:
let! v1 = newVar'
James
Hi mate, great stuff. Is there any C# or Java code available for this program? I'm trying to explore Type Inference stuffs and landed here. It looks interesting.
Post a Comment