bidir.fs

// Bidirectional typechecking

type Type =
    | Bool
    | Fun of Type * Type

type Term =
    | Var of string
    | App of Term * Term
    | Lam of string * Term
    | True
    | False
    | If of Term * Term * Term
    | Ann of Term * Type

let rec lookup ctx x =
    match ctx with
    | [] -> None
    | (id, ty) :: t ->
        if id = x then Some ty
        else lookup t x

let insert ctx x ty =
    (x, ty) :: ctx

let rec inferType ctx = function
    | Var x -> lookup ctx x
    | True | False -> Some Bool
    | If (t1, t2, t3) ->
        match inferType ctx t1, inferType ctx t2, inferType ctx t3 with
        | Some Bool, Some ty2, Some ty3 -> if ty2 = ty3 then Some ty2 else None
        | _ -> None
    | Ann (x, ty) -> checkType ctx ty x
    | App (t1, t2) ->
        match inferType ctx t1 with
        | Some (Fun (ty1, ty2)) ->
            match checkType ctx ty1 t2 with
            | Some _ -> Some ty2
            | _ -> None
        | _ -> None
    | _ -> None

and checkType ctx ty = function
    | If (t1, t2, t3) ->
        match checkType ctx Bool t1, checkType ctx ty t2, checkType ctx ty t3 with
        | Some Bool, Some _, Some _ -> Some ty
        | _ -> None
    | Lam (x, t2) ->
        match ty with
        | Fun (ty1, ty2) ->
            match checkType (insert ctx x ty1) ty2 t2 with
            | Some _ -> Some ty
            | _ -> None
        | _ -> None
    | x ->
        match inferType ctx x with
        | Some ity ->
            if ity = ty then Some ty
            else None
        | _ -> None

If (True, False, True)                       |> inferType [] |> (=) (Some Bool)               |> printfn "%A"
True                                         |> inferType [] |> (=) (Some Bool)               |> printfn "%A"
Ann (True, Bool)                             |> inferType [] |> (=) (Some Bool)               |> printfn "%A"
Ann (Lam ("x", Var ("x")), Bool)             |> inferType [] |> (=) (None)                    |> printfn "%A"
Ann (Lam ("x", Var ("x")), Fun (Bool, Bool)) |> inferType [] |> (=) (Some (Fun (Bool, Bool))) |> printfn "%A"