linear types in elm v1

Lang.elm

module Lang exposing (..)

import Dict exposing (Dict)
import Type exposing (..)


type Lit
    = IntLit Int
    | CharLit Char


type Expr
    = Lit Lit
    | Var String
    | App Expr Expr
    | Lam ( String, Type ) Expr
    | Cons String (List Expr)


plus5 : Expr
plus5 =
    App (Var "+") (Lit (IntLit 5))


{-| Maps variables to types
-}
type alias Context =
    Dict String Type


idIntLambda : Expr
idIntLambda =
    -- \x : Int -> x
    Lam ( "x", intType ) (Var "x")


constIntLambda : Expr
constIntLambda =
    -- \(x : Int) (y : Int) -> x
    Lam ( "x", intType ) (Lam ( "y", intType ) (Var "x"))


defaultContext : Context
defaultContext =
    -- + : Int -> Int -> Int
    -- inc : Int -> Int
    [ ( "+", FuncType intType (FuncType intType intType) )
    , ( "inc", FuncType intType intType )
    ]
        |> Dict.fromList


type alias Error =
    String


typeCheck : ConsContext -> Context -> Expr -> Result Error ( Context, Type )
typeCheck consContext context expr =
    case expr of
        Var x ->
            Dict.get x context
                |> Result.fromMaybe "Variable not found or moved"
                |> Result.map
                    (\ty ->
                        ( Dict.remove x context, ty )
                    )

        Lit (IntLit _) ->
            Ok ( context, intType )

        Lit (CharLit _) ->
            Ok ( context, charType )

        Lam ( var, ty ) body ->
            typeCheck consContext (Dict.insert var ty context) body
                |> Result.andThen
                    (\( newContext, resType ) ->
                        case Dict.get var newContext of
                            Just _ ->
                                Err ("Unused variable: " ++ var ++ " in lambda body: " ++ exprToString body)

                            Nothing ->
                                Ok ( newContext, FuncType ty resType )
                    )

        App e1 e2 ->
            typeCheck consContext context e1
                |> Result.andThen
                    (\( newContext, ty1 ) ->
                        typeCheck consContext newContext e2
                            |> Result.andThen
                                (\( newNewContext, ty2 ) ->
                                    case ty1 of
                                        FuncType u v ->
                                            if u == ty2 then
                                                Ok ( newNewContext, v )

                                            else
                                                Err ("mismatched argument types: " ++ typeToString u ++ ", " ++ typeToString ty2)

                                        _ ->
                                            Err "whoops"
                                )
                    )

        Cons name args ->
            case Dict.get name consContext of
                Just ( constructorDef, typeDef, type_ ) ->
                    typeCheckConstructor consContext context args constructorDef.params
                        |> Result.map (\newContext -> ( newContext, type_ ))

                Nothing ->
                    Err "Constructor definition not found"


typeCheckConstructor : ConsContext -> Context -> List Expr -> List Type -> Result String Context
typeCheckConstructor consContext context args paramTypes =
    case ( args, paramTypes ) of
        ( arg :: restArgs, expectedType :: restTypes ) ->
            typeCheck consContext context arg
                |> Result.andThen
                    (\( newContext, actualType ) ->
                        if actualType == expectedType then
                            typeCheckConstructor consContext newContext restArgs restTypes

                        else
                            Err <| "Expected: " ++ typeToString expectedType ++ ", but got: " ++ typeToString actualType
                    )

        ( [], [] ) ->
            Ok context

        ( _, _ ) ->
            Err
                "Wrong number of arguments for constructor"



---- Convenience shit ----


isLambda : Expr -> Bool
isLambda expr =
    case expr of
        Lam _ _ ->
            True

        _ ->
            False


isApp : Expr -> Bool
isApp expr =
    case expr of
        App _ _ ->
            True

        _ ->
            False


parensIf : Bool -> String -> String
parensIf b s =
    if b then
        "(" ++ s ++ ")"

    else
        s


tc : Expr -> String
tc e =
    typeCheck defaultConsContext defaultContext e
        |> Result.map Tuple.second
        |> Result.map typeToString
        |> collapse


collapse : Result x x -> x
collapse res =
    case res of
        Ok x ->
            x

        Err x ->
            x



---- Print stuff ----


litToString : Lit -> String
litToString lit =
    case lit of
        IntLit i ->
            String.fromInt i

        CharLit c ->
            String.fromChar c


exprToString : Expr -> String
exprToString e =
    let
        go shouldUseLambda expr =
            case expr of
                Var x ->
                    x

                Lit lit ->
                    litToString lit

                Lam ( var, ty ) body ->
                    let
                        prefix =
                            if shouldUseLambda then
                                "\\"

                            else
                                ""

                        arrow =
                            if isLambda body then
                                " "

                            else
                                " -> "
                    in
                    prefix ++ parensIf True (var ++ " : " ++ typeToString ty) ++ arrow ++ go (not (isLambda body)) body

                App e1 e2 ->
                    parensIf (isLambda e1) (go True e1) ++ " " ++ parensIf (isApp e2) (go True e2)

                Cons name args ->
                    name
                        ++ (args
                                |> List.map (\s -> " " ++ exprToString s)
                                |> String.join ""
                           )
    in
    go True e

Type.elm

module Type exposing (..)

{-| Types are what you put in a type annotation:

                            BaseType "Char" : Type
                            |
                            vvvv
      x : (Int -> String) -> Char
            ^^^^^^^^^^
            |
        FuncType Int String : Type

    TypeDefs are a representation of adt definitions:

      type IntOrChar =
            | MakeInt Int
            | MakeChar Char
    Becomes

        { name = "IntOrChar"
        , constructors =
            [ { name = "MakeInt"
            , params = [ BaseType "Int" ]
            }
            , { name = "MakeChar"
            , params = [ BaseType "Char" ]
            }
            ]
        } : TypeDef

-}

import Dict exposing (Dict)


type Type
    = BaseType String
    | FuncType Type Type -- Linear?


type alias Constructor =
    { name : String
    , params : List Type
    }


type alias TypeDef =
    { name : String
    , constructors : List Constructor
    }


charType : Type
charType =
    BaseType "Char"


intType : Type
intType =
    BaseType "Int"


charOrIntType : Type
charOrIntType =
    BaseType "CharOrFloat"


charOrIntDef : TypeDef
charOrIntDef =
    { name = "CharOrFloat"
    , constructors =
        [ { name = "MakeChar"
          , params = [ charType ]
          }
        , { name = "MakeInt"
          , params = [ intType ]
          }
        ]
    }


typeDefToString : TypeDef -> String
typeDefToString def =
    "type "
        ++ def.name
        ++ " =\n"
        ++ (def.constructors
                |> List.map (\cons -> "\t| " ++ constructorToString cons)
                |> String.join "\n"
           )


constructorToString : Constructor -> String
constructorToString constructor =
    constructor.name
        ++ (constructor.params
                |> List.map (\ty -> " " ++ typeToString ty)
                |> String.join ""
           )


typeToString : Type -> String
typeToString ty =
    case ty of
        BaseType name ->
            name

        FuncType ((FuncType _ _) as argType) resType ->
            "(" ++ typeToString argType ++ ")" ++ " -> " ++ typeToString resType

        FuncType argType resType ->
            typeToString argType ++ " -> " ++ typeToString resType



--------


{-| Maps constructor names to typedefs and types
-}
type alias ConsContext =
    Dict String ( Constructor, TypeDef, Type )


defaultConsContext : ConsContext
defaultConsContext =
    charOrIntDef.constructors
        |> List.map (\cons -> ( cons.name, ( cons, charOrIntDef, charOrIntType ) ))
        |> Dict.fromList