Блог

Я хотел бы расширить алгоритм W на вывод кортежей и списков в F #, априори, нужно добавить только два правила, что я и сделал, однако результат частично плохой.

Действительно, если я протестирую код, подобный этому:

 test = (8, "Hello", 0.3)  -- test :: (TInt, TString, TFloat)
id :: a -> a
id x = x                  -- id :: a -> a
foo = id 8                -- foo :: TInt
 

с другой стороны, как подробно описано в примерах ниже, подобный код работать не будет:

 makePair = (x -> (x, x)) -- makePair :: a -> (a, a)
pair = makePair 7
 

и pair будет выведен как (a, a) вместо (TInt, TInt) .

То же самое для списков.

Я использовал эту статью для написания моей проверки типов.

Я действительно не понимаю, что заклинивает. Вот минимальная функциональная программа, используемая для этих примеров:

Вывод.fs

 module Typechecker

    type Identifier = string
    and Expr =
        | Var of Identifier
        | Lambda of Identifier * Expr
        | Apply of Expr * Expr
        | Let of Identifier * Expr * Expr
        | Literal of Literal
        | Tuple of Expr list
        | List of Expr list
    and Literal =
        | Int of int
        | Float of float
        | String of string
    and Statement =
        | Signature of Identifier * Type
        | Declaration of Identifier * Expr
    and Type =
        | TVar of Identifier
        | TInt
        | TFloat
        | TString
        | TArrow of Type * Type
        | TTuple of Type list
        | TList of Type

    type Program = Program of Statement list

    type Scheme = Scheme of string list * Type
    and TypeEnv = Map<Identifier, Scheme>
    and Subst = Map<string, Type>

    type Env =
        { mutable _functions: Function list }
          with

               member this.containsFunction name =
                    this._functions |> List.exists (fun f -> f._name = name)

               member this.getFunction name =
                    this._functions
                    |> List.find (fun (f: Function) -> f._name = name)

               member this.getFunctionType name =
                    (this.getFunction name)._type

               member this.hasFunctionImplementation name =
                    if this.containsFunction name
                    then (this.getFunction name)._value.IsSome
                    else false

               member this.getFunctionValue name =
                    (this.getFunction name)._value.Value

               /// Updates the value of a function in the environment
               member this.updateFunction_value name value =
                    (this.getFunction name)._value <- Some value
                    this

               /// Updates the type of a function in the environment
               member this.updateFunction_type name ty =
                    (this.getFunction name)._type <- ty
                    this

               member this.addFunction name ty value =
                    { _functions =
                        List.append
                            this._functions
                            [{ _name = name;
                               _type = ty;
                               _value = value }] }

    and Function =
        { _name: Identifier;
          mutable _type: Type;
          mutable _value: Expr option }

    and DataType =
        { _name: Identifier;
          _isAlias: bool;
          _constructors: Ctor list option
          _alias: Type option }

    and Ctor = Term of Identifier | Product of Type list

    let newEnv = { _functions = [] }

    module Type =
        let rec ftv = function
            | TInt -> Set.empty
            | TFloat -> Set.empty
            | TString -> Set.empty
            | TVar name -> Set.singleton name
            | TArrow(t1, t2) -> Set.union (ftv t1) (ftv t2)
            | TTuple ts -> List.fold (fun acc t -> Set.union acc (ftv t)) Set.empty ts
            | TList t -> Set.singleton (toString t)

        and apply s t =
            match t with
            | TVar name ->
                match Map.tryFind name s with
                | Some t -> t
                | None -> TVar name
            | TArrow (t1, t2) ->
                TArrow(apply s t1, apply s t2)
            | TInt | TFloat | TString -> t
            | _ -> t

        and parens s =
            sprintf "(%s)" s

        and braces s =
            sprintf "{ %s }" s

        and toString t =
            let rec parenType t' =
                match t' with
                | TArrow(_, _) -> parens (toString t')
                | _ -> toString t'

            match t with
                | TVar name -> name
                | TInt -> "Integer"
                | TFloat -> "Float"
                | TString -> "String"
                | TArrow(t1, t2) ->
                    (parenType t1)   " -> "   (toString t2)
                | TTuple ts -> sprintf "(%s)" (System.String.Join(", ", List.map toString ts))
                | TList t -> sprintf "[%s]" (toString t)

    module Scheme =
        let rec ftv (scheme: Scheme) =
            match scheme with
            | Scheme(variables, t) ->
                Set.difference(Type.ftv t) (Set.ofList variables)

        and apply (s: Subst) (scheme: Scheme) =
            match scheme with
            | Scheme(variables, t) ->
                let newSubst = List.foldBack (fun key currentSubst -> Map.remove key currentSubst) variables s
                let newType = Type.apply newSubst t
                Scheme(variables, newType)

    module TypeEnv =
        let rec remove (env: TypeEnv) (var: Identifier) =
            Map.remove var env

        and ftv (typeEnv: TypeEnv) =
            Seq.foldBack (fun (KeyValue(_, v)) state ->
                Set.union state (Scheme.ftv v)) typeEnv Set.empty

        and apply (s: Subst) (env: TypeEnv) =
            Map.map (fun _ value -> Scheme.apply s value) env

    module Subst =
        let compose s1 s2 =
            Map.union (Map.map (fun _ (v: Type) -> Type.apply s1 v) s2) s1


    let rec generalize (env: TypeEnv) (t: Type) =
        let variables =
            Set.difference (Type.ftv t) (TypeEnv.ftv env)
            |> Seq.toList
        Scheme(variables, t)


    and private currentId = ref 'a'

    and nextId () =
        let id = !currentId
        currentId := (char ((int !currentId)   1))
        id

    and resetId () = currentId := 'a'

    and newTyVar () =
       TVar(sprintf "%c" (nextId ()))

    and instantiate (ts: Scheme) =
        match ts with
        | Scheme(variables, t) ->
            let nvars = variables |> List.map (fun name -> newTyVar ())
            let s = List.zip variables nvars |> Map.ofList
            Type.apply s t

    and varBind a t =
        match t with
        | TVar name when name = a -> Map.empty
        | _ when Set.contains a (Type.ftv t) ->
            failwithf "Occur check fails: `%s` vs `%s`" a (Type.toString t)
        | _ -> Map.singleton a t

    and unify (t1: Type) (t2: Type) : Subst =
        match t1, t2 with
        | TVar a, t | t, TVar a -> varBind a t
        | TInt, TInt -> Map.empty
        | TFloat, TFloat -> Map.empty
        | TString, TString -> Map.empty
        | TArrow(l, r), TArrow(l', r') ->
            let s1 = unify l l'
            let s2 = unify (Type.apply s1 r) (Type.apply s1 r')
            Subst.compose s2 s1
        | TTuple ts, TTuple ts' ->
            if ts.Length <> ts'.Length
            then failwithf "Types do not unify: `%s` vs `%s`" (Type.toString t1) (Type.toString t2)
            else List.fold Subst.compose Map.empty (List.map2 unify ts ts')
        | TList t, TList t' ->
            unify t t'
        | _ -> failwithf "Types do not unify: `%s` vs `%s`" (Type.toString t1) (Type.toString t2)

    and tiLit = function
        | Literal.Int _ -> Type.TInt
        | Literal.Float _ -> Type.TFloat
        | Literal.String _ -> Type.TString

    and tiExpr (env: TypeEnv) (exp: Expr) : Subst * Type =
        match exp with
        | Var name ->
            match Map.tryFind name env with
            | Some sigma ->
                let t = instantiate sigma
                (Map.empty, t)
            | None -> failwithf "Unbound variable: `%s`" name
        | Literal lit -> (Map.empty, tiLit lit)
        | Let(id, expr, in') ->
            let s1, t1 = tiExpr env expr
            let env1 = TypeEnv.remove env id
            let scheme = generalize (TypeEnv.apply s1 env) t1
            let env2 = Map.add id scheme env1
            let s2, t2 = tiExpr (TypeEnv.apply s1 env2) in'
            (Subst.compose s2 s1, t2)
        | Lambda(id, value) ->
            let tv = newTyVar ()
            let env1 = TypeEnv.remove env id
            let env2 = Map.union env1 (Map.singleton id (Scheme([], tv)))
            let s1, t1 = tiExpr env2 value
            (s1, TArrow(Type.apply s1 tv, t1))
        | Tuple values ->
            (Map.empty, TTuple(List.map (fun v -> snd (tiExpr env v)) values))
        | List ts ->
            let tv = newTyVar ()
            if ts.IsEmpty
            then (Map.empty, TList tv)
            else
                let _, t1 = tiExpr env ts.[0]
                if List.forall (fun t -> snd (tiExpr env t) = t1) ts
                then (Map.empty, TList t1)
                else failwith "Not all items in the list are of the same type"
        | Apply(e1, e2) ->
            let s1, t1 = tiExpr env e1
            let s2, t2 = tiExpr (TypeEnv.apply s1 env) e2
            let tv = newTyVar ()
            let s3 = unify (Type.apply s2 t1) (TArrow(t2, tv))
            (Subst.compose (Subst.compose s3 s2) s1, Type.apply s3 tv)

    and expression_typeInference env exp =
        let s, t = tiExpr env exp
        Type.apply s t

    and updateExprEnv (env: Env) =
        let mutable env' = Map.empty
        List.iter
            (fun (f: Function) ->
                env' <- env'.Add(f._name, Scheme([f._name], f._type))
            ) env._functions
        env'

    let rec public statement_typecheck (env: Env) stmt =

        let exprEnv = updateExprEnv env

        match stmt with
        | Signature(id, dastType) ->
            typecheck_signature env id dastType
        | Declaration(id, value) ->
            typecheck_decl env id value exprEnv


    and private typecheck_signature (env: Env) id ty =
        if env.hasFunctionImplementation id
        then failwithf "The type of a function cannot be defined after its implementation (`%s`)" id
        else env.addFunction id ty None

    and private typecheck_decl (env: Env) id value exprEnv =
        let _, t_exp = tiExpr exprEnv value
        if env.containsFunction id
        then if env.hasFunctionImplementation id
             then failwithf "Already declared function: `%s`" id
             else
                let t_sgn = (env.getFunction id)._type
                let unapp = try (Type.apply ((unify t_sgn t_exp)) t_exp)
                                |> Ok with exn -> failwithf "%s" exn.Message
                if match unapp with Result.Ok _ -> true
                then env.updateFunction_value id value
                else failwithf "The signature of `%s` is different than the type of its valuen  (`%s` vs `%s`)"
                               id (Type.toString t_sgn) (Type.toString t_exp)
        else env.addFunction id t_exp (Some value)


    let typecheck_document (document: Program) =
        let mutable docenv = newEnv
        match document with Program stmts ->
            List.iter (fun stmt -> docenv <- statement_typecheck docenv stmt) stmts
        docenv
 

Main.fs

 module Main
    open Inference

    [<EntryPoint>]
    let main _ =

        let test1 =
            [Declaration("makePair", Lambda("x", Tuple([Var "x"; Var "x"]))); // makePair = (x -> (x, x))
             Declaration("pair", Apply(Var "makePair", Literal (Int 7)))]     // pair = makePair 7
        let infer1 = typecheck_document (Program test1)
        printfn "Env1: %A" infer1

        let test2 =
            [Signature("id", TArrow(TVar "a", TVar "a"));                     // id :: a -> a
             Declaration("id", Lambda("x", Var "x"))                          // id x = x
             Declaration("foo", Apply(Var "id", Literal (Int 7)))]            // foo = id 7
        let infer2 = typecheck_document (Program test2)
        printfn "Env2: %A" infer2

        0
 

Вот результат:

 Env1: {_functions =
  [{_name = "makePair";
    _type = TArrow (TVar "a",TTuple [TVar "a"; TVar "a"]);
    _value = Some (Lambda ("x",Tuple [Var "x"; Var "x"]));};
   {_name = "pair";
    _type = TTuple [TVar "a"; TVar "a"];
    _value = Some (Apply (Var "makePair",Literal (Int 7)));}];}
Env2: {_functions =
  [{_name = "id";
    _type = TArrow (TVar "a",TVar "a");
    _value = Some (Lambda ("x",Var "x"));};
   {_name = "test";
    _type = TInt;
    _value = Some (Apply (Var "id",Literal (Int 7)));}];}
 

Таким образом, мы можем видеть, что вывод работает правильно для первого теста, но не для второго (как показано выше).

Я хотел бы решить и понять эту ошибку, и я заранее благодарю вас за вашу помощь.

Насколько я читал в вашем коде, похоже, что вам не хватает ветки apply .

Действительно, когда t это a Tuple [] , вы в основном возвращаете его … что, конечно, не сработает. 🙂

Я предлагаю добавить одну ветвь к совпадению, с t помощью a Tuple types , с a map (t -> apply s t) types (извините, я не очень разбираюсь в синтаксисе F #).

Надеюсь, это поможет. 🙂