A typechecker for SystemF (without existential type), uses α-conversion to perform capture-free subtitution

SystemF.fs

type SystemFType =
    | TVariable of name : string
    | TArrow of domain : SystemFType * result : SystemFType
    | TUniversal of binder : string * body : SystemFType
    
    override this.ToString() = 
        let rec aux = function
            | TVariable name -> name
            | TArrow (domain, result) ->
                match domain with
                | TVariable _ -> $"%s{aux domain} -> %s{aux result}"
                | _ -> $"(%s{aux domain}) -> %s{aux result}"
            | TUniversal (binder, body) -> $"forall %s{binder}. %s{aux body}"
        aux this
    
type SystemFTerm =
    | EVariable of name : string
    | EAbstraction of binder : string * binderType : SystemFType * body : SystemFTerm
    | EApplication of f : SystemFTerm * argument : SystemFTerm
    | ETypeAbstraction of binder : string * body : SystemFTerm
    | ETypeApplication of f : SystemFTerm * argument : SystemFType
    
type SystemFContextBinding =
    | VTermBinding of name : string * termType : SystemFType
    | VTypeBinding of name : string
    
type SystemFContext = List<SystemFContextBinding>

type UniqueStringGenerator () =
    let mutable counter = 0
    
    member this.Generate (excludes : Set<string>) =
        let rec loop () =
            let candidate = "x" + counter.ToString()
            counter <- counter + 1
            if excludes.Contains(candidate) then loop () else candidate
        in loop ()

let uniqueStringGenerator = UniqueStringGenerator()
        
let rec fv = function
    | EVariable name -> Set.singleton name
    | EAbstraction (binder, _, body) ->
        Set.ofSeq [ for i in fv body do if i <> binder then yield i ]
    | EApplication (f, argument) ->
        Set.union (fv f) (fv argument)
    | ETypeAbstraction (_, body) -> fv body
    | ETypeApplication (f, _) -> fv f
    
let rec fvType = function
    | TVariable name -> Set.singleton name
    | TArrow (domain, result) ->
        Set.union (fvType domain) (fvType result)
    | TUniversal (binder, body) ->
        Set.ofSeq [ for i in fvType body do if i <> binder then yield i ]
        
let rec substitute (term : SystemFTerm) (name : string) (replacement : SystemFTerm) : SystemFTerm = 
    match term with
    | EVariable name' ->
        if name = name' then replacement else term
    | EAbstraction (binder, _, systemFTerm) ->
        if name = binder then term
        else if (fv replacement).Contains(binder) then
            let newBinder = uniqueStringGenerator.Generate(Set.union (fv replacement) (fv systemFTerm))
            let newSystemFTerm = substitute systemFTerm binder (EVariable newBinder)
            EAbstraction(newBinder, TVariable newBinder, substitute newSystemFTerm name replacement)
        else
            EAbstraction(binder, TVariable binder, substitute systemFTerm name replacement)
    | EApplication (f, argument) ->
        EApplication(substitute f name replacement, substitute argument name replacement)
    | ETypeAbstraction (binder, systemFTerm) -> ETypeAbstraction(binder, substitute systemFTerm name replacement)
    | ETypeApplication (f, argument) -> ETypeApplication(substitute f name replacement, argument)
    
let rec substituteType (termType : SystemFType) (name : string) (replacement : SystemFType) : SystemFType = 
    match termType with
    | TVariable name' ->
        if name = name' then replacement else termType
    | TArrow (domain, result) ->
        TArrow(substituteType domain name replacement, substituteType result name replacement)
    | TUniversal (binder, body) ->
        if name = binder then termType
        else if (fvType replacement).Contains(binder) then
            let newBinder = uniqueStringGenerator.Generate(Set.union (fvType replacement) (fvType body))
            let newBody = substituteType body binder (TVariable newBinder)
            TUniversal(newBinder, substituteType newBody name replacement)
        else
            TUniversal(binder, substituteType body name replacement)
            
let findBinding (context : SystemFContext) (name : string) : SystemFContextBinding option =
    context |> List.tryFind (function
        | SystemFContextBinding.VTermBinding(name', _) -> name = name'
        | SystemFContextBinding.VTypeBinding name' -> name = name')            

let rec typeOf (term : SystemFTerm) (context : SystemFContext) : SystemFType =
    match term with
    | EVariable name ->
        match findBinding context name with
        | Some(SystemFContextBinding.VTermBinding(_, termType)) -> termType
        | _ -> failwithf $"Variable %s{name} is not bound"
    | EAbstraction (binder, binderType, body) ->
        let newContext = SystemFContextBinding.VTermBinding(binder, binderType) :: context
        TArrow(binderType, typeOf body newContext)
    | EApplication (f, argument) ->
        let fType = typeOf f context
        let argumentType = typeOf argument context
        match fType with
        | TArrow (domain, result) ->
            if domain = argumentType then result
            else failwithf $"Type mismatch: expected %A{domain}, got %A{argumentType}"
        | _ -> failwithf $"Type mismatch: expected arrow type, got %A{fType}"
    | ETypeAbstraction (binder, body) ->
        let newContext = SystemFContextBinding.VTypeBinding binder :: context
        TUniversal(binder, typeOf body newContext)
    | ETypeApplication (systemFTerm, systemFType) ->
        match typeOf systemFTerm context with
        | TUniversal (binder, body) -> substituteType body binder systemFType
        | _ -> failwithf $"Type mismatch: expected universal type, got %A{typeOf systemFTerm context}"
       
let double = ETypeAbstraction("X",
    EAbstraction("f", TArrow(TVariable "X", TVariable "X"),
        EAbstraction("a", TVariable "X",
            EApplication(EVariable "f", EApplication(EVariable "f", EVariable "a")))))

let doubleInt = ETypeApplication(double, TVariable "int")

printfn $"%A{(typeOf double []).ToString()}"
printfn $"%A{(typeOf doubleInt []).ToString()}"