tyschemehelpers.fs

let rec tysubst theta t =
    match t with
    | TVarExpr u ->
        match Map.tryFind u theta with
        | Some t' -> t'
        | None -> t
    | TApExpr (l, r) ->
        TApExpr (tysubst theta l, tysubst theta r)
    | _ ->
        t

let n = ref 1
let freshpolytyvar kind =
    let ret = TyVar (sprintf "t%i" !n, kind)
    n := !n + 1
    ret

let freshtyvar _ =
    freshpolytyvar Star

let instantiate (Forall (formals, tau)) actuals =
    tysubst (Map.ofList (List.zip formals actuals)) tau

let rec freevars t =
    match t with
    | TVarExpr u -> Set.singleton u
    | TApExpr (l, r) -> Set.union (freevars l) (freevars r)
    | TConExpr _ -> Set.empty

let generalize skipTyVars tau =
    let ts = freevars tau
    Forall (Set.difference ts skipTyVars |> List.ofSeq, tau)