Sunday 15 August 2010

Hindley Milner Type Inference Sample Implementation

// 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())

Sunday 20 June 2010

Subsequences of a seq<'a>

let cons x xs = seq { yield x
                      yield! xs }

let (|Empty|Cons|) xs : Choice<Unit, 'a * seq<'a>> =
     if (Seq.isEmpty xs) then
        Empty
      else
        Cons(Seq.head xs, Seq.skip 1 xs)

let rec subseq xs =
    match xs with
    | Empty -> seq[seq[]]
    | Cons(x,xs) -> let subseq = subseq xs
                    Seq.append (Seq.map (cons x) subseq) subseq

open System
open FsCheck

type MyGenerators =
    static member Seq() =
        let fsList = Arb.Default.FsList()
        {new Arbitrary<seq<'a>>() with
            override x.Generator =
                Gen.resize 10 (Gen.map (List.toSeq) (fsList.Generator))
            override x.Shrinker t =
                Seq.map (List.toSeq) (fsList.Shrinker(Seq.toList t)) }

ignore (Arb.register<MyGenerators>())

Check.Quick (fun xs -> (Seq.length (subseq xs) =
                       int (Math.Pow(2.0, (float (Seq.length xs))))))