expresso (empty) → 0.1.0.0
raw patch · 15 files changed
+3498/−0 lines, 15 filesdep +basedep +containersdep +directory
Dependencies added: base, containers, directory, expresso, filepath, hashable, haskeline, mtl, parsec, tasty, tasty-hunit, text, unordered-containers, wl-pprint
Files
- CHANGELOG.md +5/−0
- LICENSE +13/−0
- Prelude.x +108/−0
- README.md +310/−0
- expresso.cabal +94/−0
- src/Expresso.hs +182/−0
- src/Expresso/Eval.hs +477/−0
- src/Expresso/Parser.hs +577/−0
- src/Expresso/Pretty.hs +49/−0
- src/Expresso/Syntax.hs +107/−0
- src/Expresso/Type.hs +420/−0
- src/Expresso/TypeCheck.hs +612/−0
- src/Expresso/Utils.hs +124/−0
- src/Repl.hs +247/−0
- src/Tests.hs +173/−0
+ CHANGELOG.md view
@@ -0,0 +1,5 @@+# Change Log++## 0.1.0.0++Initial release.
+ LICENSE view
@@ -0,0 +1,13 @@+Note: This license has also been called the "New BSD License" or "Modified BSD License". See also the 2-clause BSD License.++Copyright 2017-2019, Tim Philip Williams++Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:++1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.++3. Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Prelude.x view
@@ -0,0 +1,108 @@+--+-- Expresso Prelude+--+let++ id = x -> x;+ const = x y -> x;+ flip = f x y -> (f y x);++ ----------------------------------------------------------------+ -- List operations++ map = f -> foldr (x xs -> f x :: xs) [];+ filter = f -> foldr (x xs -> if f x then (x::xs) else xs);+ length = foldr (const (n -> 1 + n)) 0;+ foldl = f z xs -> foldr (x xsf r -> xsf (f r x)) id xs z;+ reverse = foldl (xs x -> x :: xs) [];+ concat = xss -> foldr (xs ys -> xs ++ ys) [] xss;+ intersperse = sep xs ->+ let f = x xs -> (if null xs then [x] else x :: sep :: xs)+ in foldr f [] xs;+ intercalate = xs xss -> concat (intersperse xs xss);++ ----------------------------------------------------------------+ -- Maybe operations - smart constructors create closed variants++ just = x -> Just x+ : forall a. a -> <Just : a, Nothing : {}>;++ nothing = Nothing{}+ : forall a. <Just : a, Nothing : {}>;++ maybe = b f m -> case m of { Just a -> f a, Nothing{} -> b }+ : forall a b. b -> (a -> b) -> <Just : a, Nothing : {}> -> b;++ isJust = maybe False (const True);+ isNothing = maybe True (const False);+ fromMaybe = x -> maybe x id;+ listToMaybe = foldr (x -> const (just x)) nothing;+ maybeToList = maybe [] (x -> [x]);+ catMaybes = xs -> concat (map maybeToList xs);+ mapMaybe = f -> maybe nothing (just << f);++ ----------------------------------------------------------------+ -- Either operations - smart constructors create closed variants++ left = x -> Left x+ : forall a b. a -> <Left : a, Right : b>;++ right = x -> Right x+ : forall a b. b -> <Left : a, Right : b>;++ either = f g m -> case m of { Left a -> f a, Right b -> g b }+ : forall a b c. (a -> c) -> (b -> c) -> <Left : a, Right : b> -> c;++ ----------------------------------------------------------------+ -- Logical operations++ and = foldr (x y -> x && y) True;+ or = foldr (x y -> x || y) False;+ any = p -> or << map p;+ all = p -> and << map p;++ elem = x -> any (x' -> x' == x);+ notElem = x -> all (x' -> x' /= x);++ ----------------------------------------------------------------+ -- Dynamic binding++ withOverride = overrides f self -> overrides (f self);+ mkOverridable = f -> { override_ = overrides -> (withOverride overrides f) | fix f};++ override = r overrides -> mkOverridable (r.override_ overrides)+++-- Exports+in { id+ , const+ , map+ , filter+ , length+ , foldl+ , reverse+ , concat+ , intercalate+ , intersperse+ , just+ , nothing+ , maybe+ , isJust+ , isNothing+ , fromMaybe+ , listToMaybe+ , maybeToList+ , catMaybes+ , mapMaybe+ , left+ , right+ , either+ , and+ , or+ , any+ , all+ , elem+ , notElem+ , mkOverridable+ , override+ }
+ README.md view
@@ -0,0 +1,310 @@+# ☕ Expresso++A simple expressions language with polymorphic extensible row types.+++## Introduction++Expresso is a minimal statically-typed functional programming language, designed with embedding and/or extensibility in mind.+Possible use cases for such a minimal language include configuration (à la Nix), data exchange (à la JSON) or even a starting point for a custom external DSL.++Expresso has the following features:++- A small and simple implementation+- Statically typed with type inference+- Structural typing with extensible records and variants+- Lazy evaluation+- Convenient use from Haskell (a type class for marshalling values)+- Haskell-inspired syntax+- Type annotations to support first-class modules and schema validation use cases+- Built-in support for ints, double, bools, chars, maybes and lists++## Installation++Expresso the library and executable (the REPL) is currently built and tested using cabal.++## Functions++Expresso is a functional language and so we use lambda terms as our basic means of abstraction. To create a named function, we simply bind a lambda using let. I toyed with the idea of using Nix-style lambda syntax, e.g. `x: x` for the identity function, but many mainstream languages, not just Haskell, use an arrow to denote a lambda term. An arrow is also consistent with the notation we use for types.+Expresso therefore uses the arrow `->` to denote lambdas, with the parameters to bind on the left and the expression body on the right, for example `x -> x` for identity.++Note that multiple juxtaposed arguments is sugar for currying. For example:++ f x -> f x++is the same as:++ f -> x -> f x++The function composition operators are `>>` and `<<` for forwards and backwards composition respectively.+++## Records++Expresso records are built upon row-types with row extension as the fundamental primitive. This gives a very simple and easy-to-use type system when compared to more advanced systems built upon concatenation as a primitive. However, even in this simple system, concatenation can be encoded quite easily using difference records.++Records can of course contain arbitrary types and be arbitrarily nested. They can also be compared for equality. The dot operator (select) is used to project out values.++ Expresso REPL+ Type :help or :h for a list of commands+ Loaded Prelude from /home/tim/Expresso/Prelude.x+ λ> {x = 1}.x+ 1+ λ> {x = {y = "foo"}, z = [1,2,3]}.x.y+ "foo"+ λ> {x = 1, y = True} == {y = True, x = 1}+ True++Note that records cannot refer to themselves, as Expresso does not support type-level recursion.++### Record extension++Records are eliminated using selection `.` and introduced using extension `|`. For example, the record literal:++ {x = 1, y = True}++is really sugar for:++ {x = 1 | { y = True | {}}}++The row types use lacks constraints to prohibit overlapping field names. For example, the following is ill-typed:++ {x = 1, x = 2} -- DOES NOT TYPE CHECK!++ let r = {x = "foo"} in {x = "bar" | r} -- DOES NOT TYPE CHECK!++The lacks constraints are shown when printing out inferred row types via the REPL, for example:++ λ> :type r -> {x = 1 | r}+ forall r. (r\x) => {r} -> {x : Int | r}++In the above output, the REPL reports that this lambda can take a record with underlying row-type `r`, providing `r` satisfies the constraint that it does not have a field `x`.++The type of a literal record is *closed*, in that the set of fields is fully known:++ λ> :type {x = 1}+ {x : Int}++However, we permit records with redundant fields as arguments to functions, by inferring *open* record types:++ λ> let sqmag = {x, y} -> x*x + y*y+ λ> :type sqmag+ forall a r. (Num a, r\x\y) => {x : a, y : a | r} -> a++An open record type is indicated by a row-type in the tail of the record.++Note that the function definition for `sqmag` above makes use of field punning. We could have alternatively written:++ λ> let sqmag = r -> r.x*r.x + r.y*r.y++### Record restriction++We can remove a field by using the restriction primitive `\`. For example, the following will type-check:++ {x = 1 | {x = 2}\x}++We can also use the following syntactic sugar, for such an override:++ {x := 1 | {x = 1}}++### First-class modules++Records can be used as a simple but powerful module system. For example, imagine a module `"List.x"` with derived operations on lists:++ let+ reverse = foldl (xs x -> x :: xs) [];+ intercalate = xs xss -> concat (intersperse xs xss);+ ...++ -- Exports+ in { reverse+ , intercalate+ , ...+ }++Such a module can be imported using a `let` declaration:++ λ> let list = import "List.x"+ λ> :type list.intercalate+ forall a. [a] -> [[a]] -> [a]++Or simply:++ λ> let {..} = import "List.x"++Records with polymorphic functions can be passed as lambda arguments and remain polymorphic using *higher-rank polymorphism*. To accomplish this, we must provide Expresso with a suitable type annotation of the argument. For example:++ let f = (m : forall a. { reverse : [a] -> [a] |_}) ->+ {l = m.reverse [True, False], r = m.reverse "abc" }++The function `f` above takes a "module" `m` containing a polymorphic function `reverse`. We annotate `m` with a type by using a single colon `:` followed by the type we are expecting.+Note the underscore `_` in the tail of the record. This is a *type wildcard*, meaning we have specified a *partial type signature*. This type wildcard allows us to pass an arbitrary module containing a `reverse` function with this signature. To see the full type signature of `f`, we can use the Expresso REPL:++ λ> :t f+ forall r. (r\reverse) => (forall a. {reverse : [a] -> [a] | r}) ->+ {l : [Bool], r : [Char]}++Note that the `r`, representing the rest of the module fields, is a top-level quantifier. The type wildcard is especially useful here, as it allows us to avoid creating a top-level signature for the entire function and explicitly naming this row variable. More generally, type wildcards allow us to leave parts of a type signature unspecified.++Function `f` can now of course be applied to any module satisfying the type signature:++ λ> f (import "Prelude.x")+ {l = [False, True], r = "cba"}+++### Difference records and concatenation++To encode concatenation, we can use functions that extend records and compose them using straightforward function composition:++ let f = (r -> { x = "foo", y = True | r}) >> (r -> { z = "bar" | r})++Expresso has a special syntax for such "difference records":++ λ> let f = {| x = "foo", y = True |} >> {| z = "bar" |}+ λ> f {}+ {z = "bar", x = "foo", y = True}++Concatenation is asymmetric whenever we use overrides, for example:++ {| x = "foo" |} >> {| x := "bar" |} -- Type checks+ {| x = "foo" |} << {| x := "bar" |} -- DOES NOT TYPE CHECK!++### The Unit type++The type `{}` is an example of a *Unit* type. It has only one inhabitant, the empty record `{}`:++ λ> :type {}+ {}+++## Variants++The dual of records are variants, which are also polymorphic and extensible since they use the same underlying row-types.+Variants are introduced via injection (the dual of record selection), for example:++ λ> Foo 1+ Foo 1++Unlike literal records, literal variants are *open*.++ λ> :type Foo 1+ forall r. (r\Foo) => <Foo : Int | r>++Variants are eliminated using the case construct, for example:++ λ> case Foo 1 of { Foo x -> x, Bar{x,y} -> x+y }+ 1++The above case expression eliminates a *closed* variant, meaning any value other than `Foo` or `Bar` with their expected payloads would lead to a type error. To eliminate an *open* variant, we use a syntax analogous to extension:++ λ> let f = x -> case x of { Foo x -> x, Bar{x,y} -> x+y | otherwise -> 42 }+ λ> f (Baz{})+ 42++Here the unmatched variant is passed to a lambda (with `otherwise` as the parameter). The expression after the bar `|` typically either ignores the variant or delegates it to another function.++### Closed variants++We will often need to create closed variant types. For example, we may want to create a structural type analogous to Haskell's `Maybe a`, having only two constructors: `Nothing` and `Just`. This can be accomplished using smart constructors with type annotations. In the Prelude, we define the equivalent constructors `just` and `nothing`, as well as a fold `maybe` over this closed set:++ just = x -> Just x : forall a. a -> <Just : a, Nothing : {}>;++ nothing = Nothing{} : forall a. <Just : a, Nothing : {}>;++ maybe = b f m -> case m of { Just a -> f a, Nothing{} -> b }+++### Variant embedding++The dual of record restriction is variant embedding. This allows us to restrict the behaviour exposed by a case expression, by exploiting the non-overlapping field constraints.+For example, to prevent use of the `Bar` alternative of function `f` above, we can define a new function `g` as follows:++ λ> let g = x -> f (<|Bar|> x)+ λ> :type g+ forall r. (r\Bar\Foo) => <Foo : Int | r> -> Int++Embedding is used internally to implement overriding alternatives, for example:++ λ> let g = x -> case x of { override Foo x -> x + 1 | f }++is sugar for:++ λ> let g = x -> case x of { Foo x -> x + 1 | <|Foo|> >> f }++ λ> :type g+ forall r1 r2. (r1\x\y, r2\Bar\Foo) => <Foo : Int, Bar : {x : Int, y : Int | r1} | r2> -> Int++### The Void type++Internally, the syntax to eliminate a closed variant uses the empty variant type `<>`, also known as *Void*. The Void type has no inhabitants, but we can use it to define a function `absurd`:++ λ> :type absurd+ forall a. <> -> a++Absurd is an example of *Ex Falso Quodlibet* from classical logic (anything can be proven using a contradiction as a premise).++As an example of the above, the following closed case expression:++ case x of { Foo{} -> 1, Bar{} -> 2 }++is actually sugar for:++ case x of { Foo{} -> 1 | x' -> case x' of { Bar{} -> 2 | absurd } }+++## A data-exchange format with schemas++We could use Expresso as a lightweight data-exchange format (i.e. JSON with types). But how might be validate terms against a schema?++A simple type annotation `<term> : <type>` , will not suffice for "schema validation". For example, consider this attempt at validating an integer against a schema that permits everything:++ 1 : forall a. a -- FAILS++The above fails to type check since the left-hand-side is inferred as the most general type (here a concrete int) and the right-hand-side must be less so.++Instead we need something like this:++ (id : forall a. a -> a) 1++A nice syntactic sugar for this is a *signature section*, although the version in Expresso is slightly different from the Haskell proposal. We write `(:T)` to mean `id : T -> T`, where any quantifiers are kept at the top-level. We can now use:++ (: forall a. a) 1++If we really do have places in our schema where we want to permit arbitrary data, we should use the equality constraint to guarantee the absence of partially-applied functions. For example:++ (: forall a. Eq a => { x : <Foo : Int, Bar : a> }) { x = Bar id }++would fail to type check. But the following succeeds:++ λ> (: forall a. Eq a => { x : <Foo : Int, Bar : a> }) { x = Bar "abc" }+ {x = Bar "abc"}+++## Lazy evaluation++Expresso uses lazy evaluation in the hope that it might lead to efficiency gains when working with large nested records.++ λ> :peek {x = "foo"}+ {x = <Thunk>}+++## Turing equivalence?++Turing equivalence is introduced via a single `fix` primitive, which can be easily removed or disabled.+`fix` can be useful to achieve open recursive records and dynamic binding (à la Nix).++ λ> let r = mkOverridable (self -> {x = "foo", y = self.x ++ "bar"})+ λ> r+ {override_ = <Lambda>, x = "foo", y = "foobar"}++ λ> override r {| x := "baz" |}+ {override_ = <Lambda>, x = "baz", y = "bazbar"}++Note that removing `fix` and Turing equivalence does not guarantee termination in practice. It is still possible to write exponential programs that will not terminate during the lifetime of the universe without recursion or fix.++## References++Expresso is built upon many ideas described in the following publications:+* "Practical type inference for arbitrary-rank types" Peyton-Jones et al. 2011.+* "A Polymorphic Type System for Extensible Records and Variants" B. R. Gaster and M. P. Jones, 1996.+* "Extensible records with scoped labels" D. Leijen, 2005.
+ expresso.cabal view
@@ -0,0 +1,94 @@+Name: expresso+Version: 0.1.0.0+Cabal-Version: >= 1.10+License: BSD3+License-File: LICENSE+Author: Tim Williams+Maintainer: info@timphilipwilliams.com+Stability: Experimental+Synopsis: A simple expressions language based on row types+Category: Configuration+Description:+ Expresso is a minimal statically-typed functional programming language, designed with embedding and/or extensibility in mind.+ .+ Possible use cases for such a minimal language include configuration (à la Nix), data exchange (à la JSON) or even a starting point for a custom external DSL.+ .+ Please refer to README.md for more information.+Build-Type: Simple+Bug-Reports: https://github.com/willtim/Expresso/issues+Extra-Source-Files:+ Prelude.x+ CHANGELOG.md+ README.md++Source-Repository head+ Type: git+ Location: https://github.com/willtim/Expresso++Library+ Hs-Source-Dirs: src+ Default-Language: Haskell2010+ Build-Depends: base >= 4.11.1 && < 4.12,+ containers >= 0.5.11 && < 0.6,+ directory >= 1.3.1 && < 1.4,+ filepath >= 1.4.2 && < 1.5,+ hashable >= 1.2.7 && < 1.3,+ text >= 1.2.3 && < 1.3,+ haskeline >= 0.7.4 && < 0.8,+ mtl >= 2.2.2 && < 2.3,+ parsec >= 3.1.13 && < 3.2,+ unordered-containers >= 0.2.9 && < 0.3,+ wl-pprint >= 1.2.1 && < 1.3+ Exposed-Modules: Expresso+ Other-Modules: Expresso.Parser+ Expresso.Eval+ Expresso.Type+ Expresso.TypeCheck+ Expresso.Syntax+ Expresso.Pretty+ Expresso.Utils+ ghc-options: -Wall -fwarn-tabs -funbox-strict-fields+ -fno-warn-orphans+ -fno-warn-unused-do-bind+ -fno-warn-name-shadowing+ -fno-warn-missing-pattern-synonym-signatures++Executable expresso+ Main-Is: Repl.hs+ Hs-Source-Dirs: src+ Default-Language: Haskell2010++ Build-Depends: base, containers, hashable, mtl, parsec, wl-pprint, text,+ unordered-containers, haskeline, directory, filepath+ Other-Modules: Expresso.Parser+ Expresso.Eval+ Expresso.Type+ Expresso.TypeCheck+ Expresso.Syntax+ Expresso.Pretty+ Expresso.Utils+ Expresso++ ghc-options: -threaded -rtsopts -Wall -fwarn-tabs -funbox-strict-fields+ -fno-warn-orphans+ -fno-warn-unused-do-bind+ -fno-warn-name-shadowing+ -fno-warn-missing-pattern-synonym-signatures++Test-Suite test-expresso+ Type: exitcode-stdio-1.0+ Main-Is: Tests.hs+ Hs-Source-Dirs: src+ Default-Language: Haskell2010++ Build-Depends: base, containers, hashable, mtl, parsec, wl-pprint, text,+ unordered-containers, haskeline, directory, filepath,+ expresso, tasty, tasty-hunit+ Other-Modules: Expresso+ Expresso.Eval+ Expresso.Parser+ Expresso.Pretty+ Expresso.Syntax+ Expresso.Type+ Expresso.TypeCheck+ Expresso.Utils
+ src/Expresso.hs view
@@ -0,0 +1,182 @@+{-# LANGUAGE TupleSections #-}+{-# OPTIONS_GHC -Wno-unused-top-binds #-}++-- |+-- Module : Expresso+-- Copyright : (c) Tim Williams 2017-2019+-- License : BSD3+--+-- Maintainer : info@timphilipwilliams.com+-- Stability : experimental+-- Portability : portable+--+-- A simple expressions language with polymorphic extensible row types.+--+-- This module is the public API for Expresso.+--+module Expresso+ ( Bind(..)+ , Env+ , Environments+ , Exp+ , ExpF(..)+ , ExpI+ , HasValue(..)+ , Import(..)+ , Name+ , Thunk(..)+ , TIState+ , TypeEnv+ , Value(..)+ , bind+ , dummyPos+ , evalFile+ , evalFile'+ , evalString+ , evalString'+ , evalWithEnv+ , initEnvironments+ , installBinding+ , runEvalM+ , showType+ , showValue+ , showValue'+ , dumpTypeEnv+ , typeOf+ , typeOfString+ , typeOfWithEnv+ , validate+ , Eval.mkStrictLam+ , Eval.mkStrictLam2+ , Eval.mkStrictLam3+ ) where++import Control.Monad ((>=>))+import Control.Monad.Except (ExceptT(..), runExceptT, throwError)++import Expresso.Eval (Env, EvalM, HasValue(..), Thunk(..), Value(..), insertEnv, runEvalM)+import Expresso.TypeCheck (TIState, initTIState)+import Expresso.Pretty (render)+import Expresso.Syntax+import Expresso.Type+import Expresso.Utils+import qualified Expresso.Eval as Eval+import qualified Expresso.TypeCheck as TypeCheck+import qualified Expresso.Parser as Parser++-- | Type and term environments.+data Environments = Environments+ { envsTypeEnv :: !TypeEnv+ , envsTIState :: !TIState+ , envsTermEnv :: !Env+ }++-- | Empty initial type and term environments.+initEnvironments :: Environments+initEnvironments = Environments mempty initTIState mempty++-- | Install a binding using the supplied name, type and term.+-- Useful for extending the set of built-in functions.+installBinding :: Name -> Type -> Value -> Environments -> Environments+installBinding name ty val envs =+ envs { envsTypeEnv = insertTypeEnv name ty (envsTypeEnv envs)+ , envsTermEnv = insertEnv name (Thunk . return $ val) (envsTermEnv envs)+ }++-- | Query the type of an expression using the supplied type environment.+typeOfWithEnv :: Environments -> ExpI -> IO (Either String Type)+typeOfWithEnv (Environments tEnv tState _) ei = runExceptT $ do+ e <- Parser.resolveImports ei+ ExceptT $ return $ inferTypes tEnv tState e++-- | Query the type of an expression.+typeOf :: ExpI -> IO (Either String Type)+typeOf = typeOfWithEnv initEnvironments++-- | Parse an expression and query its type.+typeOfString :: String -> IO (Either String Type)+typeOfString str = runExceptT $ do+ top <- ExceptT $ return $ Parser.parse "<unknown>" str+ ExceptT $ typeOf top++-- | Evaluate an expression using the supplied type and term environments.+evalWithEnv+ :: HasValue a+ => Environments+ -> ExpI+ -> IO (Either String a)+evalWithEnv (Environments tEnv tState env) ei = runExceptT $ do+ e <- Parser.resolveImports ei+ _sigma <- ExceptT . return $ inferTypes tEnv tState e+ ExceptT $ runEvalM . (Eval.eval env >=> Eval.proj) $ e++-- | Evaluate the contents of the supplied file path; and optionally+-- validate using a supplied type (schema).+evalFile :: HasValue a => Maybe Type -> FilePath -> IO (Either String a)+evalFile = evalFile' initEnvironments++-- | Evaluate the contents of the supplied file path; and optionally+-- validate using a supplied type (schema).+-- NOTE: This version also takes a term environment and a type environment+-- so that foreign functions and their types can be installed respectively.+evalFile' :: HasValue a => Environments -> Maybe Type -> FilePath -> IO (Either String a)+evalFile' envs mty path = runExceptT $ do+ top <- ExceptT $ Parser.parse path <$> readFile path+ ExceptT $ evalWithEnv envs (maybe id validate mty $ top)++-- | Parse an expression and evaluate it; optionally+-- validate using a supplied type (schema).+evalString :: HasValue a => Maybe Type -> String -> IO (Either String a)+evalString = evalString' initEnvironments++-- | Parse an expression and evaluate it; optionally+-- validate using a supplied type (schema).+-- NOTE: This version also takes a term environment and a type environment+-- so that foreign functions and their types can be installed respectively.+evalString' :: HasValue a => Environments -> Maybe Type -> String -> IO (Either String a)+evalString' envs mty str = runExceptT $ do+ top <- ExceptT $ return $ Parser.parse "<unknown>" str+ ExceptT $ evalWithEnv envs (maybe id validate mty $ top)++-- | Add a validating type signature section to the supplied expression.+validate :: Type -> ExpI -> ExpI+validate ty e = Parser.mkApp pos (Parser.mkSigSection pos ty) [e]+ where+ pos = dummyPos++-- | Used by the REPL to bind variables.+bind+ :: Environments+ -> Bind Name+ -> ExpI+ -> EvalM Environments+bind (Environments tEnv tState env) b ei = do+ e <- Parser.resolveImports ei+ let (res'e, tState') =+ TypeCheck.runTI (TypeCheck.tcDecl (getAnn ei) b e) tEnv tState+ case res'e of+ Left err -> throwError err+ Right tEnv' -> do+ thunk <- Eval.mkThunk $ Eval.eval env e+ env' <- Eval.bind env b thunk+ return $ Environments tEnv' tState' env'++-- | Pretty print the supplied type.+showType :: Type -> String+showType = render . ppType++-- | Pretty print the supplied value. This does *not* evaluate deeply.+showValue :: Value -> String+showValue = render . Eval.ppValue++-- | Pretty print the supplied value. This evaluates deeply.+showValue' :: Value -> IO String+showValue' v = either id render <$> (runEvalM $ Eval.ppValue' v)++-- | Extract type environment bindings.+dumpTypeEnv :: Environments -> [(Name, Sigma)]+dumpTypeEnv = typeEnvToList . envsTypeEnv++inferTypes :: TypeEnv -> TIState -> Exp -> Either String Type+inferTypes tEnv tState e =+ fst $ TypeCheck.runTI (TypeCheck.typeCheck e) tEnv tState
+ src/Expresso/Eval.hs view
@@ -0,0 +1,477 @@+{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -Wno-unused-top-binds #-} + +-- | +-- Module : Expresso.Eval +-- Copyright : (c) Tim Williams 2017-2019 +-- License : BSD3 +-- +-- Maintainer : info@timphilipwilliams.com +-- Stability : experimental +-- Portability : portable +-- +-- A lazy evaluator. +-- +-- The front-end syntax is simple, so we evaluate it directly. +-- +module Expresso.Eval( + Env + , EvalM + , HasValue(..) + , Thunk(..) + , Value(..) + , bind + , eval + , insertEnv + , mkStrictLam + , mkStrictLam2 + , mkStrictLam3 + , mkThunk + , ppValue + , ppValue' + , runEvalM +) +where + +import Control.Monad.Except +import Data.Foldable (foldrM) +import Data.HashMap.Strict (HashMap) +import Data.IORef +import Data.Ord +import Data.Text (Text) +import qualified Data.Text as T +import qualified Data.HashMap.Strict as HashMap +import qualified Data.List as List + +import Expresso.Syntax +import Expresso.Type +import Expresso.Pretty +import Expresso.Utils (cata, (:*:)(..), K(..)) + +-- | A call-by-need environment. +-- Using a HashMap makes it easy to support record wildcards. +newtype Env = Env { unEnv :: HashMap Name Thunk } deriving (Semigroup, Monoid) + +type EvalM a = ExceptT String IO a + +-- | A potentially unevaluated value. +newtype Thunk = Thunk { force :: EvalM Value } + +instance Show Thunk where + show _ = "<Thunk>" + +mkThunk :: EvalM Value -> EvalM Thunk +mkThunk ev = do + ref <- liftIO $ newIORef Nothing + return $ Thunk $ do + mv <- liftIO $ readIORef ref + case mv of + Nothing -> do + v <- ev + liftIO $ writeIORef ref (Just v) + return v + Just v -> return v + +-- | Type for an evaluated term. +data Value + = VLam !(Thunk -> EvalM Value) + | VInt !Integer + | VDbl !Double + | VBool !Bool + | VChar !Char + | VText !Text + | VList ![Value] -- lists are strict + | VRecord !(HashMap Label Thunk) -- field order no defined + | VVariant !Label !Thunk + +-- | This does *not* evaluate deeply +ppValue :: Value -> Doc +ppValue (VLam _) = "<Lambda>" +ppValue (VInt i) = integer i +ppValue (VDbl d) = double d +ppValue (VBool b) = if b then "True" else "False" +ppValue (VChar c) = text $ '\'' : c : '\'' : [] +ppValue (VText s) = string (show $ T.unpack s) +ppValue (VList xs) = bracketsList $ map ppValue xs +ppValue (VRecord m) = bracesList $ map ppEntry $ HashMap.keys m + where + ppEntry l = text l <+> "=" <+> "<Thunk>" +ppValue (VVariant l _) = text l <+> "<Thunk>" + +-- | This evaluates deeply +ppValue' :: Value -> EvalM Doc +ppValue' (VRecord m) = (bracesList . map ppEntry . HashMap.toList) + <$> mapM (force >=> ppValue') m + where + ppEntry (l, v) = text l <+> text "=" <+> v +ppValue' (VVariant l t) = (text l <+>) <$> (force >=> ppParensValue) t +ppValue' v = return $ ppValue v + +ppParensValue :: Value -> EvalM Doc +ppParensValue v = + case v of + VVariant{} -> parens <$> ppValue' v + _ -> ppValue' v + +extractChar :: Value -> Maybe Char +extractChar (VChar c) = Just c +extractChar _ = Nothing + +-- | Run the EvalM evaluation computation. +runEvalM :: EvalM a -> IO (Either String a) +runEvalM = runExceptT + +eval :: Env -> Exp -> EvalM Value +eval env e = cata alg e env + where + alg :: (ExpF Name Bind Type :*: K Pos) (Env -> EvalM Value) + -> Env + -> EvalM Value + alg (EVar v :*: _) env = lookupValue env v >>= force + alg (EApp f x :*: K pos) env = do + f' <- f env + x' <- mkThunk (x env) + evalApp pos f' x' + alg (ELam b e1 :*: _ ) env = evalLam env b e1 + alg (EAnnLam b _ e1 :*: _) env = evalLam env b e1 + alg (ELet b e1 e2 :*: _) env = do + t <- mkThunk $ e1 env + env' <- bind env b t + e2 env' + alg (EPrim p :*: K pos) _ = return $ evalPrim pos p + alg (EAnn e _ :*: _) env = e env + +evalLam :: Env -> Bind Name -> (Env -> EvalM Value) -> EvalM Value +evalLam env b e = return $ VLam $ \x -> + bind env b x >>= e + +evalApp :: Pos -> Value -> Thunk -> EvalM Value +evalApp _ (VLam f) t = f t +evalApp pos fv _ = + throwError $ show pos ++ " : Expected a function, but got: " ++ + show (ppValue fv) + +evalPrim :: Pos -> Prim -> Value +evalPrim pos p = case p of + Int i -> VInt i + Dbl d -> VDbl d + Bool b -> VBool b + Char c -> VChar c + Text s -> VText s + Show -> mkStrictLam $ \v -> VText . T.pack . show <$> ppValue' v + -- Trace + ErrorPrim -> VLam $ \s -> do + msg <- proj' s + throwError $ "error (" ++ show pos ++ "): " ++ msg + + ArithPrim Add -> mkStrictLam2 $ numOp pos (+) + ArithPrim Sub -> mkStrictLam2 $ numOp pos (-) + ArithPrim Mul -> mkStrictLam2 $ numOp pos (*) + ArithPrim Div -> mkStrictLam2 $ \v1 v2 -> + case (v1, v2) of + (VInt x, VInt y) -> return $ VInt $ x `div` y + (VDbl x, VDbl y) -> return $ VDbl $ x / y + _ -> failOnValues pos [v1, v2] + + RelPrim RGT -> mkStrictLam2 $ \v1 v2 -> + (VBool . (==GT)) <$> compareValues pos v1 v2 + + RelPrim RGTE -> mkStrictLam2 $ \v1 v2 -> + (VBool . (`elem` [GT, EQ])) <$> compareValues pos v1 v2 + + RelPrim RLT -> mkStrictLam2 $ \v1 v2 -> + (VBool . (==LT)) <$> compareValues pos v1 v2 + + RelPrim RLTE -> mkStrictLam2 $ \v1 v2 -> + (VBool . (`elem` [LT, EQ])) <$> compareValues pos v1 v2 + + Eq -> mkStrictLam2 $ \v1 v2 -> + VBool <$> equalValues pos v1 v2 + + NEq -> mkStrictLam2 $ \v1 v2 -> + (VBool . not) <$> equalValues pos v1 v2 + + Not -> VLam $ \v -> VBool <$> proj' v + And -> VLam $ \v1 -> return $ VLam $ \v2 -> + VBool <$> ((&&) <$> proj' v1 <*> proj' v2) + + Or -> VLam $ \v1 -> return $ VLam $ \v2 -> + VBool <$> ((||) <$> proj' v1 <*> proj' v2) + + Double -> mkStrictLam $ \v -> + case v of + VInt i -> return $ VDbl $ fromInteger i + _ -> failOnValues pos [v] + Floor -> mkStrictLam $ \v -> + case v of + VDbl d -> return $ VInt $ floor d + _ -> failOnValues pos [v] + Ceiling -> mkStrictLam $ \v -> + case v of + VDbl d -> return $ VInt $ ceiling d + _ -> failOnValues pos [v] + + Neg -> mkStrictLam $ \v -> + case v of + VInt i -> return $ VInt $ negate i + VDbl d -> return $ VDbl $ negate d + _ -> failOnValues pos [v] + + Mod -> mkStrictLam $ \v1 -> return $ mkStrictLam $ \v2 -> + case (v1, v2) of + (VInt x, VInt y) -> return $ VInt $ x `mod` y + _ -> failOnValues pos [v1, v2] + + Cond -> VLam $ \c -> return $ VLam $ \t -> return $ VLam $ \f -> + proj' c >>= \c -> if c then force t else force f + FixPrim -> mkStrictLam $ \f -> fix (evalApp pos f <=< mkThunk) + + -- We cannot yet define operators like this in the language + FwdComp -> mkStrictLam2 $ \f g -> + return $ VLam $ \x -> + mkThunk (evalApp pos f x) >>= evalApp pos g + BwdComp -> mkStrictLam2 $ \f g -> + return $ VLam $ \x -> + mkThunk (evalApp pos g x) >>= evalApp pos f + + Pack -> mkStrictLam $ packChars pos + Unpack -> mkStrictLam $ unpackChars pos + + ListEmpty -> VList [] + ListNull -> VLam $ \xs -> + (VBool . (null :: [Value] -> Bool)) <$> proj' xs + ListCons -> VLam $ \x -> return $ VLam $ \xs -> + VList <$> ((:) <$> force x <*> proj' xs) + ListAppend -> VLam $ \xs -> return $ VLam $ \ys -> + VList <$> ((++) <$> proj' xs <*> proj' ys) + ListFoldr -> mkStrictLam $ \f -> + return $ VLam $ \z -> return $ VLam $ \xs -> do + let g a b = do g' <- evalApp pos f (Thunk $ return a) + evalApp pos g' (Thunk $ return b) + z' <- force z + xs' <- proj' xs :: EvalM [Value] + foldrM g z' xs' + + RecordExtend l -> VLam $ \v -> return $ VLam $ \r -> + (VRecord . HashMap.insert l v) <$> proj' r + RecordRestrict l -> VLam $ \r -> + (VRecord . HashMap.delete l) <$> proj' r + RecordSelect l -> VLam $ \r -> do + r' <- proj' r + let err = throwError $ show pos ++ " : " ++ l ++ " not found" + maybe err force (HashMap.lookup l r') + RecordEmpty -> VRecord mempty + + VariantInject l -> VLam $ \v -> + return $ VVariant l v + VariantEmbed _ -> VLam force + VariantElim l -> mkStrictLam $ \f -> return $ mkStrictLam2 $ \k s -> do + case s of + VVariant l' t | l==l' -> evalApp pos f t + | otherwise -> evalApp pos k (Thunk $ return s) + v -> throwError $ show pos ++ " : Expected a variant, but got: " ++ + show (ppValue v) + Absurd -> VLam $ \v -> force v >> throwError "The impossible happened!" + p -> error $ show pos ++ " : Unsupported Prim: " ++ show p + +-- non-strict bind +bind :: Env -> Bind Name -> Thunk -> EvalM Env +bind env b t = case b of + Arg n -> return $ insertEnv n t env + _ -> bind' env b t + +-- strict bind +bind' :: Env -> Bind Name -> Thunk -> EvalM Env +bind' env b t = do + v <- force t + case (b, v) of + (Arg n, _) -> + return $ insertEnv n (Thunk $ return v) env + (RecArg ns, VRecord m) | Just vs <- mapM (\n -> HashMap.lookup n m) ns -> + return $ env <> (mkEnv $ zip ns vs) + (RecWildcard, VRecord m) -> + return $ env <> Env m + _ -> throwError $ "Cannot bind the pair: " ++ show b ++ " = " ++ show (ppValue v) + +insertEnv :: Name -> Thunk -> Env -> Env +insertEnv n t (Env m) = Env $ HashMap.insert n t m + +lookupEnv :: Name -> Env -> Maybe Thunk +lookupEnv n (Env m) = HashMap.lookup n m + +mkEnv :: [(Name, Thunk)] -> Env +mkEnv = Env . HashMap.fromList + +lookupValue :: Env -> Name -> EvalM Thunk +lookupValue env n = maybe err return $ lookupEnv n env + where + err = throwError $ "Not found: " ++ show n + +failOnValues :: Pos -> [Value] -> EvalM a +failOnValues pos vs = throwError $ show pos ++ " : Unexpected value(s) : " ++ + show (parensList (map ppValue vs)) + +-- | Make a strict Expresso lambda value (forced arguments) from a +-- Haskell lambda. +mkStrictLam :: (Value -> EvalM Value) -> Value +mkStrictLam f = VLam $ \x -> force x >>= f + +-- | As mkStrictLam, but accepts Haskell functions with two curried arguments. +mkStrictLam2 :: (Value -> Value -> EvalM Value) -> Value +mkStrictLam2 f = mkStrictLam $ \v -> return $ mkStrictLam $ f v + +-- | As mkStrictLam, but accepts Haskell functions with three curried arguments. +mkStrictLam3 :: (Value -> Value -> Value -> EvalM Value) -> Value +mkStrictLam3 f = mkStrictLam $ \v -> return $ mkStrictLam2 $ f v + +proj' :: HasValue a => Thunk -> EvalM a +proj' = force >=> proj + +numOp :: Pos -> (forall a. Num a => a -> a -> a) -> Value -> Value -> EvalM Value +numOp _ op (VInt x) (VInt y) = return $ VInt $ x `op` y +numOp _ op (VDbl x) (VDbl y) = return $ VDbl $ x `op` y +numOp p _ v1 v2 = failOnValues p [v1, v2] + +-- NB: evaluates deeply +equalValues :: Pos -> Value -> Value -> EvalM Bool +equalValues _ (VInt i1) (VInt i2) = return $ i1 == i2 +equalValues _ (VDbl d1) (VDbl d2) = return $ d1 == d2 +equalValues _ (VBool b1) (VBool b2) = return $ b1 == b2 +equalValues _ (VChar c1) (VChar c2) = return $ c1 == c2 +equalValues _ (VText s1) (VText s2) = return $ s1 == s2 +equalValues p (VList xs) (VList ys) + | length xs == length ys = and <$> zipWithM (equalValues p) xs ys + | otherwise = return False +equalValues p (VRecord m1) (VRecord m2) = do + (ls1, vs1) <- unzip . recordValues <$> mapM force m1 + (ls2, vs2) <- unzip . recordValues <$> mapM force m2 + if length ls1 == length ls2 && length vs1 == length vs2 + then and <$> zipWithM (equalValues p) vs1 vs2 + else return False +equalValues p (VVariant l1 v1) (VVariant l2 v2) + | l1 == l2 = join $ equalValues p <$> force v1 <*> force v2 + | otherwise = return False +equalValues p v1 v2 = failOnValues p [v1, v2] + +-- NB: evaluates deeply +compareValues :: Pos -> Value -> Value -> EvalM Ordering +compareValues _ (VInt i1) (VInt i2) = return $ compare i1 i2 +compareValues _ (VDbl d1) (VDbl d2) = return $ compare d1 d2 +compareValues _ (VBool b1) (VBool b2) = return $ compare b1 b2 +compareValues _ (VChar c1) (VChar c2) = return $ compare c1 c2 +compareValues _ (VText s1) (VText s2) = return $ compare s1 s2 +compareValues p (VList xs) (VList ys) = go xs ys + where + go :: [Value] -> [Value] -> EvalM Ordering + go [] [] = return EQ + go (_:_) [] = return GT + go [] (_:_) = return LT + go (x:xs') (y:ys') = do + c <- compareValues p x y + if c == EQ + then go xs' ys' + else return c +compareValues p v1 v2 = failOnValues p [v1, v2] + +-- | Used for equality of records, sorts values by key +recordValues :: HashMap Label a -> [(Label, a)] +recordValues = List.sortBy (comparing fst) . HashMap.toList + +packChars :: Pos -> Value -> EvalM Value +packChars pos (VList xs) + | Just cs <- mapM extractChar xs = return . VText . T.pack $ cs + | otherwise = failOnValues pos xs +packChars pos v = failOnValues pos [v] + +unpackChars :: Pos -> Value -> EvalM Value +unpackChars _ (VText s) = return . VList . map VChar . T.unpack $ s +unpackChars pos v = failOnValues pos [v] + +------------------------------------------------------------ +-- HasValue class and instances + +-- TODO generic derivation a la GG + +-- TODO write pure evaluator in ST, carry type in class to get rid of Either/Maybe to get +-- instance (HasValue b) => HasValue (a -> b) where +instance (HasValue a, HasValue b) => HasValue (a -> EvalM b) where + proj (VLam f) = return $ \x -> do + r <- f (Thunk $ return $ inj x) + proj r + proj v = failProj "VLam" v + inj f = VLam $ \v -> proj' v >>= fmap inj . f + +-- | A class of Haskell types that can be projected from or injected +-- into Expresso values. +class HasValue a where + proj :: Value -> EvalM a + inj :: a -> Value + +instance HasValue Value where + proj v = return v + inj = id + +instance HasValue Integer where + proj (VInt i) = return i + proj v = failProj "VInt" v + inj = VInt + +instance HasValue Double where + proj (VDbl d) = return d + proj v = failProj "VDbl" v + inj = VDbl + +instance HasValue Bool where + proj (VBool b) = return b + proj v = failProj "VBool" v + inj = VBool + +instance HasValue Char where + proj (VChar c) = return c + proj v = failProj "VChar" v + inj = VChar + +instance HasValue Text where + proj (VText s) = return s + proj v = failProj "VText" v + inj = VText + +instance {-# OVERLAPS #-} HasValue a => HasValue [a] where + proj (VList xs) = mapM proj xs + proj v = failProj "VList" v + inj = VList . map inj + +instance {-# OVERLAPS #-} HasValue [Value] where + proj (VList xs) = return xs + proj v = failProj "VList" v + inj = VList + +instance HasValue a => HasValue (HashMap Name a) where + proj (VRecord m) = mapM proj' m + proj v = failProj "VRecord" v + inj = VRecord . fmap (Thunk . return . inj) + +instance {-# OVERLAPS #-} HasValue a => HasValue [(Name, a)] where + proj v = HashMap.toList <$> proj v + inj = inj . HashMap.fromList + +instance {-# OVERLAPS #-} HasValue (HashMap Name Thunk) where + proj (VRecord m) = return m + proj v = failProj "VRecord" v + inj = VRecord + +instance {-# OVERLAPS #-} HasValue [(Name, Thunk)] where + proj v = HashMap.toList <$> proj v + inj = inj . HashMap.fromList + +failProj :: String -> Value -> EvalM a +failProj desc v = throwError $ "Expected a " ++ desc ++ + ", but got: " ++ show (ppValue v)
+ src/Expresso/Parser.hs view
@@ -0,0 +1,577 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ViewPatterns #-}+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}++-- |+-- Module : Expresso.Parser+-- Copyright : (c) Tim Williams 2017-2019+-- License : BSD3+--+-- Maintainer : info@timphilipwilliams.com+-- Stability : experimental+-- Portability : portable+--+-- Parsers for Expresso terms and types.+--+module Expresso.Parser where++import Control.Applicative+import Control.Monad+import Control.Monad.Except+import Data.Maybe+import Text.Parsec hiding (many, optional, parse, (<|>))+import Text.Parsec.Language (emptyDef)+import qualified Data.Map as M+import qualified Data.Set as S+import qualified Data.Text as T+import qualified Text.Parsec as P+import qualified Text.Parsec.Expr as P+import qualified Text.Parsec.Token as P++import Expresso.Pretty (Doc, (<+>), render, parensList, text, dquotes, vcat)+import Expresso.Syntax+import Expresso.Type+import Expresso.Utils++------------------------------------------------------------+-- Resolve imports++resolveImports :: ExpI -> ExceptT String IO Exp+resolveImports = cataM alg where+ alg (InR (K (Import path)) :*: _) = do+ res <- ExceptT $ readFile path >>= return . parse path+ resolveImports res+ alg (InL e :*: pos) = return $ Fix (e :*: pos)++------------------------------------------------------------+-- Parser++parse :: SourceName -> String -> Either String ExpI+parse src = showError . P.parse (topLevel pExp) src++topLevel p = whiteSpace *> p <* P.eof++pExp = addTypeAnnot+ <$> getPosition+ <*> pExp'+ <*> optional (reservedOp ":" *> pTypeAnn)++addTypeAnnot pos e (Just t) = withPos pos (EAnn e t)+addTypeAnnot _ e Nothing = e++pExp' = pImport+ <|> pLam+ <|> pAnnLam+ <|> pLet+ <|> pCond+ <|> pCase+ <|> pOpExp+ <?> "expression"++pImport = mkImport+ <$> getPosition+ <*> (reserved "import" *> stringLiteral)+ <?> "import"++pLet = reserved "let" *>+ (flip (foldr mkLet) <$> (semiSep1 ((,) <$> getPosition <*> pLetDecl))+ <*> (reserved "in" *> pExp))+ <?> "let expression"++pLetDecl = (,) <$> pLetBind+ <*> (reservedOp "=" *> pExp <* whiteSpace)++pLam = mkLam+ <$> getPosition+ <*> try (many1 pBind <* reservedOp "->" <* whiteSpace)+ <*> pExp'+ <?> "lambda expression"++pAnnLam = mkAnnLam+ <$> getPosition+ <*> try (many1 pAnnBind <* reservedOp "->" <* whiteSpace)+ <*> pExp'+ <?> "lambda expression with type annotated argument"++pAnnBind = parens $ (,) <$> pBind <*> (reservedOp ":" *> pTypeAnn)++pAtom = pPrim <|> try pVar <|> parens (pSection <|> pExp)++pSection = pSigSection++pSigSection = mkSigSection <$> getPosition <*> (reservedOp ":" *> pTypeAnn)++pVar = mkVar <$> getPosition <*> identifier++pPrim = pNumber <|>+ pBool <|>+ pChar <|>+ pDifferenceRecord <|>+ pRecord <|>+ pVariant <|>+ pVariantEmbed <|>+ pList <|>+ pString <|>+ pPrimFun++pCond = (\pos -> mkTertiaryOp pos Cond)+ <$> getPosition+ <*> (reserved "if" *> pExp)+ <*> (reserved "then" *> pExp)+ <*> (reserved "else" *> pExp)+ <?> "if expression"++pOpExp = P.buildExpressionParser opTable pApp++-- NB: assumes "-1" and "+1" are not valid terms+pApp = mkApp <$> getPosition <*> pTerm <*> many pTerm++pTerm = mkRecordRestrict+ <$> getPosition+ <*> ((\pos -> foldl (mkRecordSelect pos))+ <$> getPosition+ <*> pAtom+ <*> try (many pSelect))+ <*> optional (reservedOp "\\" *> identifier)++opTable = [ [ prefix "-" Neg+ ]+ , [ binary ">>" FwdComp P.AssocRight+ , binary "<<" BwdComp P.AssocRight+ ]+ , [ binary "*" (ArithPrim Mul) P.AssocLeft+ , binary "/" (ArithPrim Div) P.AssocLeft+ ]+ , [ binary "+" (ArithPrim Add) P.AssocLeft+ , binary "-" (ArithPrim Sub) P.AssocLeft+ ]+ , [ binary "++" ListAppend P.AssocLeft+ , binary "::" ListCons P.AssocRight+ ]+ , [ binary "==" Eq P.AssocLeft+ , binary "/=" NEq P.AssocLeft+ , binary ">" (RelPrim RGT) P.AssocLeft+ , binary ">=" (RelPrim RGTE) P.AssocLeft+ , binary "<" (RelPrim RLT) P.AssocLeft+ , binary "<=" (RelPrim RLTE) P.AssocLeft+ ]+ , [ binary "&&" And P.AssocRight+ ]+ , [ binary "||" Or P.AssocRight+ ]+ ]++pPrimFun = msum+ [ fun "error" ErrorPrim+ , fun "show" Show+ , fun "not" Not+ , fun "foldr" ListFoldr+ , fun "null" ListNull+ , fun "fix" FixPrim+ , fun "double" Double+ , fun "floor" Floor+ , fun "ceiling" Ceiling+ , fun "abs" Abs+ , fun "mod" Mod+ , fun "absurd" Absurd+ , fun "pack" Pack+ , fun "unpack" Unpack+ ]+ where+ fun sym prim = reserved sym *> ((\pos -> mkPrim pos prim) <$> getPosition)++binary sym prim =+ P.Infix $ reservedOp sym *> ((\pos -> mkBinOp pos prim) <$> getPosition)+prefix sym prim =+ P.Prefix $ reservedOp sym *> ((\pos -> mkUnaryOp pos prim) <$> getPosition)++pSelect = reservedOp "." *> identifier++pNumber = (\pos -> either (mkInteger pos) (mkDouble pos))+ <$> getPosition+ <*> naturalOrFloat++pBool = (\pos -> mkPrim pos . Bool)+ <$> getPosition+ <*> (reserved "True" *> pure True <|>+ reserved "False" *> pure False)++pChar = (\pos -> mkPrim pos . Char)+ <$> getPosition+ <*> charLiteral++pString = (\pos -> mkPrim pos . Text . T.pack)+ <$> getPosition+ <*> stringLiteral++pBind = Arg <$> identifier+ <|> RecArg <$> pFieldPuns++pLetBind = try (RecWildcard <$ reservedOp "{..}") <|> pBind++pFieldPuns = braces $ pRecordLabel `sepBy` comma++data Entry = Extend Label ExpI | Update Label ExpI++pRecord = (\pos -> fromMaybe (mkRecordEmpty pos))+ <$> getPosition+ <*> (braces $ optionMaybe pRecordBody)++pRecordBody = mkRecordExtend <$> getPosition <*> pRecordEntry <*> pRest+ where+ pRest = (comma *> pRecordBody) <|>+ (reservedOp "|" *> pExp) <|>+ (mkRecordEmpty <$> getPosition)++pDifferenceRecord = mkDifferenceRecord+ <$> getPosition+ <*> (try (reservedOp "{|") *> (pRecordEntry `sepBy1` comma)+ <* reservedOp "|}")++mkDifferenceRecord :: Pos -> [Entry] -> ExpI+mkDifferenceRecord pos entries =+ withPos pos $ ELam (Arg "#r") $+ foldr (mkRecordExtend pos) (withPos pos $ EVar "#r") entries++pRecordEntry =+ try (Extend <$> pRecordLabel <*> (reservedOp "=" *> pExp)) <|>+ try (Update <$> pRecordLabel <*> (reservedOp ":=" *> pExp)) <|>+ mkFieldPun <$> getPosition <*> pRecordLabel++pRecordLabel = lowerIdentifier++pVariant = mkVariant <$> getPosition <*> pVariantLabel++pVariantEmbed = mkVariantEmbed+ <$> getPosition+ <*> (try (reservedOp "<|") *> (pEmbedEntry `sepBy1` comma)+ <* reservedOp "|>")+ <?> "variant embed expression"+ where+ pEmbedEntry = (,) <$> getPosition <*> pVariantLabel++pCase = mkCase <$> getPosition+ <*> (reserved "case" *> pApp <* reserved "of")+ <*> (braces pCaseBody)+ <?> "case expression"++pCaseBody = mkCaseAlt <$> getPosition <*> pCaseAlt <*> pRest+ where+ pRest = (comma *> pCaseBody) <|>+ (reservedOp "|" *> pExp) <|>+ (\pos -> mkPrim pos Absurd) <$> getPosition++pCaseAlt =+ (try (Extend <$> pVariantLabel+ <*> (whiteSpace *> pLam)) <|>+ try (Update <$> (reserved "override" *> pVariantLabel)+ <*> (whiteSpace *> pLam)))+ <?> "case alternative"++pVariantLabel = upperIdentifier++pList = brackets pListBody+ where+ pListBody = (\pos -> foldr mkListCons (mkListEmpty pos))+ <$> getPosition+ <*> ((,) <$> getPosition <*> pExp) `sepBy` comma+ <?> "list expression"++mkImport :: Pos -> FilePath -> ExpI+mkImport pos path = withAnn pos $ InR $ K $ Import path++mkInteger :: Pos -> Integer -> ExpI+mkInteger pos = mkPrim pos . Int++mkDouble :: Pos -> Double -> ExpI+mkDouble pos = mkPrim pos . Dbl++mkCase :: Pos -> ExpI -> ExpI -> ExpI+mkCase pos scrutinee caseF = mkApp pos caseF [scrutinee]++mkCaseAlt :: Pos -> Entry -> ExpI -> ExpI+mkCaseAlt pos (Extend l altLamE) contE =+ mkApp pos (mkPrim pos $ VariantElim l) [altLamE, contE]+mkCaseAlt pos (Update l altLamE) contE =+ mkApp pos (mkPrim pos $ VariantElim l)+ [ altLamE+ , mkLam pos [Arg "#r"]+ (mkApp pos contE [mkEmbed $ withPos pos $ EVar "#r"])+ ]+ where+ mkEmbed e = mkApp pos (mkPrim pos $ VariantEmbed l) [e]++mkVariant :: Pos -> Label -> ExpI+mkVariant pos l = mkPrim pos $ VariantInject l++mkVariantEmbed :: Pos -> [(Pos , Label)] -> ExpI+mkVariantEmbed pos ls =+ withPos pos $ ELam (Arg "#r") $+ foldr f (withPos pos $ EVar "#r") ls+ where+ f (pos, l) k = mkApp pos (mkPrim pos $ VariantEmbed l) [k]++mkLam :: Pos -> [Bind Name] -> ExpI -> ExpI+mkLam pos bs e =+ foldr (\b e -> withPos pos (ELam b e)) e bs++mkAnnLam :: Pos -> [(Bind Name, Type)] -> ExpI -> ExpI+mkAnnLam pos bs e =+ foldr (\(b, t) e -> withPos pos (EAnnLam b t e)) e bs++-- | signature section+-- (:T) becomes (x -> x : T -> T)+mkSigSection :: Pos -> Type -> ExpI+mkSigSection pos ty =+ withPos pos $ EAnn (mkLam pos [Arg "x"] (mkVar pos "x")) ty'+ where+ ty' = case ty of+ (Fix (TForAllF tvs t :*: K pos)) ->+ withAnn pos (TForAllF tvs (withAnn pos (TFunF t t)))+ t -> withAnn (getAnn t) (TFunF t t)++mkVar :: Pos -> Name -> ExpI+mkVar pos name = withPos pos (EVar name)++mkLet :: (Pos, (Bind Name, ExpI)) -> ExpI -> ExpI+mkLet (pos, (b, e1)) e2 = withPos pos (ELet b e1 e2)++mkTertiaryOp :: Pos -> Prim -> ExpI -> ExpI -> ExpI -> ExpI+mkTertiaryOp pos p x y z = mkApp pos (mkPrim pos p) [x, y, z]++mkBinOp :: Pos -> Prim -> ExpI -> ExpI -> ExpI+mkBinOp pos p x y = mkApp pos (mkPrim pos p) [x, y]++mkUnaryOp :: Pos -> Prim -> ExpI -> ExpI+mkUnaryOp pos p x = mkApp pos (mkPrim pos p) [x]++mkRecordSelect :: Pos -> ExpI -> Label -> ExpI+mkRecordSelect pos r l = mkApp pos (mkPrim pos $ RecordSelect l) [r]++mkRecordExtend :: Pos -> Entry -> ExpI -> ExpI+mkRecordExtend pos (Extend l e) r =+ mkApp pos (mkPrim pos $ RecordExtend l) [e, r]+mkRecordExtend pos (Update l e) r =+ mkApp pos (mkPrim pos $ RecordExtend l) [e, mkRecordRestrict pos r $ Just l]++mkRecordEmpty :: Pos -> ExpI+mkRecordEmpty pos = mkPrim pos RecordEmpty++mkRecordRestrict :: Pos -> ExpI -> Maybe Label -> ExpI+mkRecordRestrict pos e = maybe e $ \l -> mkApp pos (mkPrim pos $ RecordRestrict l) [e]++mkFieldPun :: Pos -> Label -> Entry+mkFieldPun pos l = Extend l (withPos pos $ EVar l)++mkListCons :: (Pos, ExpI) -> ExpI -> ExpI+mkListCons (pos, x) xs = mkApp pos (mkPrim pos ListCons) [x, xs]++mkListEmpty :: Pos -> ExpI+mkListEmpty pos = mkPrim pos ListEmpty++mkApp :: Pos -> ExpI -> [ExpI] -> ExpI+mkApp pos f = foldl (\g -> withPos pos . EApp g) f++mkPrim :: Pos -> Prim -> ExpI+mkPrim pos p = withPos pos $ EPrim p++withPos :: Pos -> ExpF Name Bind Type ExpI -> ExpI+withPos pos = withAnn pos . InL++------------------------------------------------------------+-- Parsers for type annotations++pTypeAnn = pType'e >>= either (fail . render) return+ where+ pType'e = unboundTyVarCheck <$> getPosition <*> pType++pType = pTForAll+ <|> pTFun+ <|> pType'++pType' = pTVar+ <|> pTInt+ <|> pTDbl+ <|> pTBool+ <|> pTChar+ <|> pTText+ <|> pTRecord+ <|> pTVariant+ <|> pTList+ <|> parens pType++pTForAll = pTForAll'e >>= either (fail . render) return+ where+ pTForAll'e = mkTForAll+ <$> getPosition+ <*> (reserved "forall" *> many1 pTyVar <* dot)+ <*> option [] (try pConstraints)+ <*> pType+ <?> "forall type annotation"++pConstraints = ((:[]) <$> pConstraint+ <|> parens (pConstraint `sepBy1` comma))+ <* reservedOp "=>"++pConstraint = pStarConstraint+ <|> pRowConstraint++pStarConstraint = (\c n -> (n, c))+ <$> (CStar <$> pStarHierarchy)+ <*> lowerIdentifier+ where+ pStarHierarchy = reserved "Eq" *> pure CEq+ <|> reserved "Ord" *> pure COrd+ <|> reserved "Num" *> pure CNum++pRowConstraint = (,)+ <$> (lowerIdentifier <* reservedOp "\\")+ <*> (lacks . (:[]) <$> identifier)++-- simple syntactic check for unbound type variables in type annotations+unboundTyVarCheck :: Pos -> Type -> Either Doc Type+unboundTyVarCheck pos t+ | not (null freeVars) = Left $ vcat+ [ ppPos pos <> ":"+ , "unbound type variable(s)" <+> parensList (map ppTyVarName freeVars) <+> "in type annotation."+ ]+ | otherwise = return t+ where+ freeVars = S.toList $ S.delete "_" (S.map tyvarName $ ftv t)+ ppTyVarName = dquotes . text++-- match up constraints and bound type variables+mkTForAll :: Pos -> [TyVar] -> [(Name, Constraint)] -> Type -> Either Doc Type+mkTForAll pos tvs (M.fromListWith unionConstraints -> m) t+ | not (null badNames) = Left $ vcat+ [ ppPos pos <> ":"+ , "constraint(s) reference unknown type variable(s):" <+> parensList (map (dquotes . text) badNames)+ ]+ | otherwise = return $ withAnn pos (TForAllF tvs' t')+ where+ t' = substTyVar tvs (map (withAnn pos . TVarF) tvs') t+ tvs' = [ maybe tv (setConstraint tv) $ M.lookup (tyvarName tv) m+ | tv <- tvs+ ]+ setConstraint tv c = tv { tyvarConstraint = c }+ bndrs = S.fromList $ map tyvarName tvs+ badNames = S.toList $ M.keysSet m S.\\ bndrs++pTVar = (\pos -> withAnn pos . TVarF)+ <$> getPosition+ <*> (pTyVar <|> pTWildcard)++pTInt = pTCon TIntF "Int"+pTDbl = pTCon TDblF "Double"+pTBool = pTCon TBoolF "Bool"+pTChar = pTCon TCharF "Char"+pTText = pTCon TTextF "Text"++pTFun = (\pos a b -> withAnn pos (TFunF a b))+ <$> getPosition+ <*> try (pType' <* reservedOp "->" <* whiteSpace) -- TODO+ <*> pType+ <?> "function type annotation"++pTCon c s = (\pos -> withAnn pos c) <$> getPosition <* reserved s++pTyVar = mkTyVar Bound <$> lowerIdentifier+pTWildcard = mkTyVar Wildcard "_" <$ reservedOp "_"++mkTyVar flavour name = TyVar flavour name (head name) CNone++pTRecord = mkFromRowType TRecordF+ <$> getPosition+ <*> (try (Just <$> braces pTVar) <|> (braces $ optionMaybe (pTRowBody pTRecordEntry)))+ <?> "record type annotation"++pTVariant = mkFromRowType TVariantF+ <$> getPosition+ <*> (try (Just <$> angles pTVar) <|> (angles $ optionMaybe (pTRowBody pTVariantEntry)))+ <?> "variant type annotation"++pTRowBody pEntry = mkTRowExtend+ <$> getPosition+ <*> pEntry+ <*> pRest+ where+ pRest = (comma *> pTRowBody pEntry) <|>+ (reservedOp "|" *> pType') <|>+ (mkTRowEmpty <$> getPosition)++mkFromRowType tCon pos =+ withAnn pos . tCon . fromMaybe (mkTRowEmpty pos)++pTRecordEntry = (,) <$> pRecordLabel <*> (reservedOp ":" *> pType)+pTVariantEntry = (,) <$> pVariantLabel <*> (reservedOp ":" *> pType)++mkTRowExtend pos (l, ty) r = withAnn pos $ TRowExtendF l ty r+mkTRowEmpty pos = withAnn pos TRowEmptyF++pTList = (\pos -> withAnn pos . TListF)+ <$> getPosition+ <*> brackets pType++------------------------------------------------------------+-- Language definition for Lexer++languageDef :: P.LanguageDef st+languageDef = emptyDef+ { P.commentStart = "{-"+ , P.commentEnd = "-}"+ , P.commentLine = "--"+ , P.nestedComments = True+ , P.identStart = letter+ , P.identLetter = alphaNum <|> oneOf "_'"+ , P.opStart = P.opLetter languageDef+ , P.opLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"+ , P.reservedOpNames= [ "->", "=", "-", "*", "/", "+"+ , "++", "::", "|", ",", ".", "\\"+ , "{|", "|}", ":=", "{..}"+ , "==", "/=", ">", ">=", "<", "<="+ , "&&", "||", ":", "=>"+ ]+ , P.reservedNames = [ "let", "in", "if", "then", "else", "case", "of"+ , "True", "False", "forall", "Eq", "Ord", "Num"+ ]+ , P.caseSensitive = True+ }+++------------------------------------------------------------+-- Lexer++lexer = P.makeTokenParser languageDef++lowerIdentifier = lookAhead lower >> identifier+upperIdentifier = lookAhead upper >> identifier++identifier = P.identifier lexer+reserved = P.reserved lexer+operator = P.operator lexer+reservedOp = P.reservedOp lexer+charLiteral = P.charLiteral lexer+stringLiteral = P.stringLiteral lexer+--natural = P.natural lexer+--integer = P.integer lexer+--float = P.float lexer+naturalOrFloat = P.naturalOrFloat lexer+--decimal = P.decimal lexer+--hexadecimal = P.hexadecimal lexer+--octal = P.octal lexer+symbol = P.symbol lexer+lexeme = P.lexeme lexer+whiteSpace = P.whiteSpace lexer+parens = P.parens lexer+braces = P.braces lexer+angles = P.angles lexer+brackets = P.brackets lexer+semi = P.semi lexer+comma = P.comma lexer+colon = P.colon lexer+dot = P.dot lexer+semiSep = P.semiSep lexer+semiSep1 = P.semiSep1 lexer+commaSep = P.commaSep lexer+commaSep1 = P.commaSep1 lexer
+ src/Expresso/Pretty.hs view
@@ -0,0 +1,49 @@+{-# LANGUAGE OverloadedStrings #-}++-- |+-- Module : Expresso.Pretty+-- Copyright : (c) Tim Williams 2017-2019+-- License : BSD3+--+-- Maintainer : info@timphilipwilliams.com+-- Stability : experimental+-- Portability : portable+--+-- Pretty printing utilities.+--+module Expresso.Pretty (+ module Text.PrettyPrint.Leijen+ , parensList+ , bracketsList+ , bracesList+ , sepBy+ , catBy+ , render+ ) where++import Data.String+import Text.PrettyPrint.Leijen ( Doc, (<+>), (<//>), angles, braces, brackets+ , comma, dot, dquotes, empty, hcat, hsep, indent+ , int, integer, double, parens, space, text, string, vcat)+import qualified Text.PrettyPrint.Leijen as PP++instance IsString Doc where+ fromString = text++bracketsList :: [Doc] -> Doc+bracketsList = brackets . hsep . PP.punctuate comma++parensList :: [Doc] -> Doc+parensList = parens . hsep . PP.punctuate comma++bracesList :: [Doc] -> Doc+bracesList = braces . hsep . PP.punctuate comma++sepBy :: Doc -> [Doc] -> Doc+sepBy d = hsep . PP.punctuate d++catBy :: Doc -> [Doc] -> Doc+catBy d = hcat . PP.punctuate d++render :: PP.Doc -> String+render doc = PP.displayS (PP.renderPretty 0.8 100 doc) []
+ src/Expresso/Syntax.hs view
@@ -0,0 +1,107 @@+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ViewPatterns #-}++-- |+-- Module : Expresso.Syntax+-- Copyright : (c) Tim Williams 2017-2019+-- License : BSD3+--+-- Maintainer : info@timphilipwilliams.com+-- Stability : experimental+-- Portability : portable+--+-- The abstract syntax for expressions in Expresso.+--+module Expresso.Syntax where++import Data.Text (Text)+import Expresso.Type+import Expresso.Utils++-- | Expressions with imports.+type ExpI = Fix ((ExpF Name Bind Type :+: K Import) :*: K Pos)++-- | Expressions with imports resolved.+type Exp = Fix (ExpF Name Bind Type :*: K Pos)++-- | An import file path.+newtype Import = Import { unImport :: FilePath }++-- | Pattern functor representing expressions and parameterised with+-- the type of variable @v@, type of binder @b@ and the type of+-- type-annotation @t@.+data ExpF v b t r+ = EVar v+ | EPrim Prim+ | EApp r r+ | ELam (b v) r+ | EAnnLam (b v) t r+ | ELet (b v) r r+ | EAnn r t+ deriving (Show, Functor, Foldable, Traversable)++-- | Binders+data Bind v+ = Arg v+ | RecArg [v]+ | RecWildcard+ deriving Show++-- | Language primitives+data Prim+ = Int Integer+ | Dbl Double+ | Bool Bool+ | Char Char+ | Text Text+ | Show+ | Trace+ | ErrorPrim+ | ArithPrim ArithOp+ | RelPrim RelOp+ | Not+ | And+ | Or+ | Eq+ | NEq+ | Double -- double from int+ | Floor+ | Ceiling+ | Abs+ | Neg+ | Mod+ | Cond+ | FixPrim+ | FwdComp+ | BwdComp+ | Pack+ | Unpack+ | ListEmpty+ | ListCons+ | ListNull -- needed if list elems have no equality defined+ | ListAppend+ | ListFoldr+ | RecordEmpty -- a.k.a. Unit+ | RecordSelect Label+ | RecordExtend Label+ | RecordRestrict Label+ | Absurd+ | VariantInject Label+ | VariantEmbed Label+ | VariantElim Label+ deriving (Eq, Ord, Show)++data ArithOp = Add | Mul | Sub | Div+ deriving (Eq, Ord, Show)++data RelOp = RGT | RGTE | RLT | RLTE+ deriving (Eq, Ord, Show)
+ src/Expresso/Type.hs view
@@ -0,0 +1,420 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE ViewPatterns #-}++-- |+-- Module : Expresso.Type+-- Copyright : (c) Tim Williams 2017-2019+-- License : BSD3+--+-- Maintainer : info@timphilipwilliams.com+-- Stability : experimental+-- Portability : portable+--+-- The abstract syntax for types in Expresso.+--+module Expresso.Type where++import Text.Parsec (SourcePos)+import Text.Parsec.Pos (newPos)++import Data.IntMap (IntMap)+import Data.Map (Map)+import Data.Set (Set)+import qualified Data.Map as M+import qualified Data.IntMap as IM+import qualified Data.Set as S++import Data.Data+import Data.Foldable (fold)++import Expresso.Pretty+import Expresso.Utils++-- | Source position+type Pos = SourcePos++-- | Row label+type Label = String++-- | A string representing a unique name.+type Name = String++-- | Type syntax annotated with source position.+type Type = Fix (TypeF :*: K Pos)++-- | Unannotated type syntax.+type Type' = Fix TypeF++type Sigma = Type+type Rho = Type -- No top-level ForAll+type Tau = Type -- No ForAlls anywhere++-- | Pattern functor for the syntax of types.+data TypeF r+ = TForAllF [TyVar] r+ | TVarF TyVar+ | TMetaVarF MetaTv+ | TIntF+ | TDblF+ | TBoolF+ | TCharF+ | TTextF+ | TFunF r r+ | TListF r+ | TRecordF r+ | TVariantF r+ | TRowEmptyF+ | TRowExtendF Label r r+ deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Typeable, Data)++type Uniq = Int++data Flavour+ = Bound -- a type variable bound by a ForAll+ | Skolem -- a skolem constant+ | Wildcard -- a type wildcard+ deriving (Eq, Ord, Show, Typeable, Data)++data TyVar = TyVar+ { tyvarFlavour :: Flavour+ , tyvarName :: Name+ , tyvarPrefix :: Char -- used to generate names+ , tyvarConstraint :: Constraint+ } deriving (Eq, Ord, Show, Typeable, Data)++data MetaTv = MetaTv -- can unify with any tau-type+ { metaUnique :: Uniq+ , metaPrefix :: Char -- used to generate names+ , metaConstraint :: Constraint+ } deriving (Eq, Ord, Show, Typeable, Data)++-- | Type variable constraints+-- e.g. for types of kind row, labels the associated tyvar must lack+data Constraint+ = CNone+ | CRow (Set Label)+ | CStar StarHierarchy+ deriving (Eq, Ord, Show, Typeable, Data)++-- | A simple hierarchy. i.e. Num has Ord and Eq, Ord has Eq.+data StarHierarchy+ = CEq+ | COrd+ | CNum+ deriving (Eq, Ord, Show, Typeable, Data)++-- | The type environment.+newtype TypeEnv = TypeEnv { unTypeEnv :: Map Name Sigma }+ deriving (Semigroup, Monoid)++insertTypeEnv :: Name -> Sigma -> TypeEnv -> TypeEnv+insertTypeEnv name ty (TypeEnv m) = TypeEnv $ M.insert name ty m++typeEnvToList :: TypeEnv -> [(Name, Sigma)]+typeEnvToList (TypeEnv m) = M.toList m++instance View TypeF Type where+ proj = left . unFix+ inj e = Fix (e :*: K dummyPos)++-- | A useless source position.+dummyPos :: Pos+dummyPos = newPos "<unknown>" 1 1++instance View TypeF Type' where+ proj = unFix+ inj = Fix++pattern TForAll vs t <- (proj -> (TForAllF vs t)) where+ TForAll vs t = inj (TForAllF vs t)+pattern TVar v <- (proj -> (TVarF v)) where+ TVar v = inj (TVarF v)+pattern TMetaVar v <- (proj -> (TMetaVarF v)) where+ TMetaVar v = inj (TMetaVarF v)+pattern TInt <- (proj -> TIntF) where+ TInt = inj TIntF+pattern TDbl <- (proj -> TDblF) where+ TDbl = inj TDblF+pattern TBool <- (proj -> TBoolF) where+ TBool = inj TBoolF+pattern TChar <- (proj -> TCharF) where+ TChar = inj TCharF+pattern TText <- (proj -> TTextF) where+ TText = inj TTextF+pattern TFun t1 t2 <- (proj -> (TFunF t1 t2)) where+ TFun t1 t2 = inj (TFunF t1 t2)+pattern TList t <- (proj -> (TListF t)) where+ TList t = inj (TListF t)+pattern TRecord t <- (proj -> (TRecordF t)) where+ TRecord t = inj (TRecordF t)+pattern TVariant t <- (proj -> (TVariantF t)) where+ TVariant t = inj (TVariantF t)+pattern TRowEmpty <- (proj -> TRowEmptyF) where+ TRowEmpty = inj TRowEmptyF+pattern TRowExtend l t1 t2 <- (proj -> (TRowExtendF l t1 t2)) where+ TRowExtend l t1 t2 = inj (TRowExtendF l t1 t2)++class Types a where+ -- | Free type variables+ ftv :: a -> Set TyVar++ -- | Meta type variables+ meta :: a -> Set MetaTv++ -- | Replace meta type variables with types+ apply :: Subst -> a -> a++instance Types Type where+ ftv = cata alg . stripAnn where+ alg :: TypeF (Set TyVar) -> (Set TyVar)+ alg (TForAllF vs t) = t S.\\ S.fromList vs+ alg (TVarF v) = S.singleton v+ alg e = fold e++ meta = cata alg . stripAnn where+ alg :: TypeF (Set MetaTv) -> (Set MetaTv)+ alg (TMetaVarF v) = S.singleton v+ alg e = fold e++ apply s t = cata alg t where+ alg :: (TypeF :*: K Pos) Type -> Type+ alg (TMetaVarF v :*: K p) =+ case IM.lookup (metaUnique v) (unSubst s) of+ Nothing -> Fix (TMetaVarF v :*: K p)+ Just t -> apply s t -- TODO could this ever fail to terminate?+ alg e = Fix e++instance Types TypeEnv where+ ftv (TypeEnv env) = ftv (M.elems env)+ meta (TypeEnv env) = meta (M.elems env)+ apply s (TypeEnv env) = TypeEnv (M.map (apply s) env)++instance Types a => Types [a] where+ ftv = foldMap ftv+ meta = foldMap meta+ apply s = map (apply s)++-- | Get all the binders used in ForAlls in the type, so that+-- when quantifying an outer forall, we can avoid these inner ones.+tyVarBndrs :: Type -> Set TyVar+tyVarBndrs = cata alg . stripAnn where+ alg :: TypeF (Set TyVar) -> (Set TyVar)+ alg (TForAllF vs t) = t <> S.fromList vs+ alg (TFunF arg res) = arg <> res+ alg _ = S.empty++-- Use to instantiate TyVars+substTyVar :: [TyVar] -> [Type] -> Type -> Type+substTyVar tvs ts t = cata alg t m where+ alg :: (TypeF :*: K Pos) (Map Name Type -> Type)+ -> Map Name Type+ -> Type+ alg (TForAllF vs f :*: K p) m =+ let m' = foldr M.delete m (map tyvarName vs)+ in Fix (TForAllF vs (f m') :*: K p)+ alg (TVarF v :*: K p) m =+ case M.lookup (tyvarName v) m of+ Nothing -> Fix (TVarF v :*: K p)+ Just t -> t+ alg e m = Fix $ fmap ($m) e++ m = M.fromList $ (map tyvarName tvs) `zip` ts++newtype Subst = Subst { unSubst :: IntMap Type }+ deriving (Show)++nullSubst :: Subst+nullSubst = Subst IM.empty++infixr 0 |->+(|->) :: MetaTv -> Type -> Subst+(|->) v t = Subst $ IM.singleton (metaUnique v) t++isInSubst :: MetaTv -> Subst -> Bool+isInSubst v = IM.member (metaUnique v) . unSubst++removeFromSubst :: [MetaTv] -> Subst -> Subst+removeFromSubst vs (Subst m) =+ Subst $ foldr IM.delete m (map metaUnique vs)++-- | apply s1 and then s2+-- NB: order is important+composeSubst :: Subst -> Subst -> Subst+composeSubst s1 s2 = Subst $ (IM.map (apply s1) $ unSubst s2) `IM.union` unSubst s1++instance Semigroup Subst where+ (<>) = composeSubst++instance Monoid Subst where+ mempty = nullSubst++-- | decompose a row-type into its constituent parts+toList :: Type -> ([(Label, Type)], Maybe Type)+toList v@TVar{} = ([], Just v)+toList v@TMetaVar{} = ([], Just v)+toList TRowEmpty = ([], Nothing)+toList (TRowExtend l t r) =+ let (ls, mv) = toList r+ in ((l, t):ls, mv)+toList t = error $ "Unexpected row type: " ++ show (ppType t)++extractMetaTv :: Type -> Maybe MetaTv+extractMetaTv (TMetaVar v) = Just v+extractMetaTv _ = Nothing++lacks :: [Label] -> Constraint+lacks = CRow . S.fromList++mkRowType :: Type -> [(Label, Type)] -> Type+mkRowType = foldr $ \(l, t@(getAnn -> pos)) r ->+ Fix (TRowExtendF l t r :*: K pos)++rowToMap :: Type -> Map Name Type+rowToMap (TRowExtend l t r) = M.insert l t (rowToMap r)+rowToMap TRowEmpty = M.empty+rowToMap TVar{} = M.empty -- default any row vars to empty row+rowToMap t = error $ "Unexpected row type: " ++ show (ppType t)+++------------------------------------------------------------+-- Constraints++-- | True if the supplied type of kind Star satisfies the supplied constraint+satisfies :: Type -> Constraint -> Bool+satisfies t c =+ case (infer t, c) of+ (CNone, CNone) -> True+ (CStar{}, CNone) -> True+ (CNone, CStar{}) -> False+ (CStar c1, CStar c2) -> c1 >= c2+ (c1, c2) -> error $ "satisfies: kind mismatch: " ++ show (c1, c2)+ where+ infer :: Type -> Constraint+ infer (TForAll _ t) = infer t+ infer (TVar v) = tyvarConstraint v+ infer (TMetaVar m) = metaConstraint m+ infer TInt = CStar CNum+ infer TDbl = CStar CNum+ infer TBool = CStar COrd+ infer TChar = CStar COrd+ infer TText = CStar COrd+ infer TFun{} = CNone+ infer (TList t) = minC (CStar COrd) (infer t)+ infer (TRecord r) =+ maybe CNone (minC (CStar CEq)) $ inferFromRow r+ infer (TVariant r) =+ maybe CNone (minC (CStar CEq)) $ inferFromRow r+ infer t = error $ "satisfies/infer: unexpected type: " ++ show t++ inferFromRow :: Type -> Maybe Constraint+ inferFromRow TVar{} = Nothing+ inferFromRow TMetaVar{} = Nothing+ inferFromRow TRowEmpty = Nothing+ inferFromRow (TRowExtend _ t r) = Just $+ maybe (infer t) (minC (infer t)) $ inferFromRow r+ inferFromRow t =+ error $ "satisfies/inferFromRow: unexpected type: " ++ show t++ minC (CStar c1) (CStar c2) = CStar $ min c1 c2+ minC CNone _ = CNone+ minC _ CNone = CNone+ minC _ _ = error "minC: assertion failed"++-- | unions constraints+-- for kind Star: picks the most specific, i.e. max c1 c2+-- for kind Row: unions the sets of lacks labels+unionConstraints :: Constraint -> Constraint -> Constraint+unionConstraints CNone c = c+unionConstraints c CNone = c+unionConstraints (CRow s1) (CRow s2) = CRow $ s1 `S.union` s2+unionConstraints (CStar c1) (CStar c2) = CStar $ max c1 c2+unionConstraints c1 c2 = error $ "unionConstraints: kind mismatch: " ++ show (c1, c2)+++------------------------------------------------------------+-- Pretty-printing++type Precedence = Int++topPrec, arrPrec, tcPrec, atomicPrec :: Precedence+topPrec = 0 -- Top-level precedence+arrPrec = 1 -- Precedence of (a->b)+tcPrec = 2 -- Precedence of (T a b)+atomicPrec = 3 -- Precedence of t++precType :: Type -> Precedence+precType (TForAll _ _) = topPrec+precType (TFun _ _) = arrPrec+precType _ = atomicPrec++-- | Print with parens if precedence arg > precedence of type itself+ppType' :: Precedence -> Type -> Doc+ppType' p t+ | p >= precType t = parens (ppType t)+ | otherwise = ppType t++ppType :: Type -> Doc+ppType (TForAll vs t) = ppForAll (vs, t)+ppType (TVar v) = text $ tyvarName v+ppType (TMetaVar v) = "v" <> int (metaUnique v)+ppType TInt = "Int"+ppType TDbl = "Double"+ppType TBool = "Bool"+ppType TChar = "Char"+ppType TText = "Text"+ppType (TFun t s) = ppType' arrPrec t <+> "->" <+> ppType' (arrPrec-1) s+ppType (TList a) = brackets $ ppType a+ppType (TRecord r) = braces $ ppRowType r+ppType (TVariant r) = angles $ ppRowType r+ppType TRowEmpty = "(||)"+ppType (TRowExtend l a r) = "(|" <> text l <> ":" <> ppType a <> "|" <> ppType r <> "|)"+ppType t = error $ "Unexpected type: " ++ show t++ppRowType :: Type -> Doc+ppRowType r = sepBy comma (map ppEntry ls)+ <> maybe mempty (ppRowTail ls) mv+ where+ (ls, mv) = toList r+ ppRowTail [] v = ppType v+ ppRowTail _ v = mempty <+> "|" <+> ppType v+ ppEntry (l, t) = text l <+> ":" <+> ppType t++ppForAll :: ([TyVar], Type) -> Doc+ppForAll (vars, t)+ | null vars = ppType' topPrec t+ | otherwise = "forall" <+> (catBy space $ map (ppType . TVar) vars) <> dot+ <> (let cs = concatMap ppConstraint vars+ in if null cs then mempty else space <> (parensList cs <+> "=>"))+ <+> ppType' topPrec t+ where+ ppConstraint :: TyVar -> [Doc]+ ppConstraint v =+ case tyvarConstraint v of+ CNone -> []+ CStar CEq -> ["Eq" <+> ppType (TVar v)]+ CStar COrd -> ["Ord" <+> ppType (TVar v)]+ CStar CNum -> ["Num" <+> ppType (TVar v)]+ CRow (S.toList -> ls)+ | null ls -> []+ | otherwise -> [catBy "\\" $ ppType (TVar v) : map text ls]++ppPos :: Pos -> Doc+ppPos = text . show++ppStarConstraint :: StarHierarchy -> Doc+ppStarConstraint CEq = "Eq"+ppStarConstraint COrd = "Ord"+ppStarConstraint CNum = "Num"
+ src/Expresso/TypeCheck.hs view
@@ -0,0 +1,612 @@+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE ViewPatterns #-}++-- |+-- Module : Expresso.TypeCheck+-- Copyright : (c) Tim Williams 2017-2019+-- License : BSD3+--+-- Maintainer : info@timphilipwilliams.com+-- Stability : experimental+-- Portability : portable+--+-- Type inference and checking.+--+-- The type system implemented here is a bi-directional Damas-Milner system extended with+-- higher-rank polymorphism, type wildcards and polymorphic extensible (constrained) row types.+--+-- The algorithm is described in detail by the tutorial paper:+-- "Practical type inference for arbitrary-rank types" Peyton-Jones et al. 2011.+--+-- The row-types extension is based on ideas from the following papers:+-- * "A Polymorphic Type System for Extensible Records and Variants" B. R. Gaster and M. P. Jones, 1996.+-- * "Extensible records with scoped labels" D. Leijen, 2005.+--+module Expresso.TypeCheck (+ typeCheck+ , tcDecl+ , runTI+ , initTIState+ , TI+ , TIState+ ) where++import qualified Data.List as L+import qualified Data.Map as M+import qualified Data.Set as S++import Control.Applicative ((<$>))+import Control.Monad.Except+import Control.Monad.Reader+import Control.Monad.State++import Expresso.Syntax+import Expresso.Type+import Expresso.Pretty+import Expresso.Utils++-- | Internal state of the inference engine.+data TIState = TIState+ { tiSupply :: Int+ , tiSubst :: Subst+ }++type TI a = ExceptT String (ReaderT TypeEnv (State TIState)) a++-- | Type check the supplied expression.+typeCheck :: Exp -> TI Sigma+typeCheck e = tcRho e Nothing >>= inferSigma (getAnn e)++-- | Run the type inference monad.+runTI :: TI a -> TypeEnv -> TIState -> (Either String a, TIState)+runTI t tEnv tState = runState (runReaderT (runExceptT t) tEnv) tState++-- | Initial state of the inference engine.+initTIState :: TIState+initTIState = TIState { tiSupply = 0, tiSubst = mempty }++fresh :: TI Int+fresh = do+ s <- get+ let i = tiSupply s+ put s {tiSupply = i + 1 }+ return i++-- Used by tcPrim+newTyVar :: Constraint -> Char -> TyVar+newTyVar c prefix = TyVar Bound [prefix] prefix c++newSkolemTyVar :: TyVar -> TI TyVar+newSkolemTyVar (TyVar _ _ prefix c) = do+ i <- fresh+ let name = prefix : show i+ return $ TyVar Skolem name prefix c++newMetaVar :: Pos -> Constraint -> Char -> TI Type+newMetaVar pos c prefix =+ annotate pos . TMetaVar <$> newMetaTyVar c prefix++newMetaTyVar :: Constraint -> Char -> TI MetaTv+newMetaTyVar c prefix = do+ i <- fresh+ return $ MetaTv i prefix c++getEnvTypes :: TI [Sigma]+getEnvTypes = (M.elems . unTypeEnv <$> ask) >>= mapM substType++substType :: Type -> TI Type+substType t = do+ s <- gets tiSubst+ return $ apply s t++lookupVar :: Pos -> Name -> TI Sigma+lookupVar pos name = do+ TypeEnv env <- ask+ case M.lookup name env of+ Just s -> return s+ Nothing -> throwError $ show $+ ppPos pos <+> ": unbound variable:" <+> text name++extendEnv :: M.Map Name Sigma -> TI a -> TI a+extendEnv binds = local (TypeEnv binds <>)++-- | Quantify over the specified type variables (all flexible).+quantify :: Pos -> [MetaTv] -> Rho -> Sigma+quantify pos mvs0 t =+ withAnn pos $ TForAllF tvs t'+ where+ -- group by prefix and number sequentially each prefix+ (mvs, tvs) = unzip+ . concat+ . M.elems+ . M.mapWithKey mkSubsts+ . M.fromListWith (++)+ . map (metaPrefix &&& (:[]))+ $ mvs0+ s = mconcat $ zipWith (|->) mvs (map TVar tvs)+ t' = apply s t++ -- avoid quantified type variables in use+ usedBndrs = map tyvarName $ S.toList $ tyVarBndrs t++ mkSubsts p mvs =+ zipWith mkSubst mvs (prefixBndrs L.\\ usedBndrs)+ where+ prefixBndrs = [p] : [ (p:show i) | i <- [(1::Integer)..]]+ mkSubst mv name =+ (mv, TyVar Bound name p (metaConstraint mv))++-- | Instantiate the topmost foralls of the argument type+-- with flexible type variables.+instantiate :: Pos -> Sigma -> TI Rho+instantiate pos (TForAll tvs t) = do+ tvs' <- mapM (\v -> newMetaTyVar (tyvarConstraint v) (tyvarPrefix v)) tvs+ let ts = map (annotate pos . TMetaVar) tvs'+ s <- gets tiSubst+ return $ substTyVar tvs ts (apply s t)+instantiate _ t = return t++-- | Performs deep skolemisation, returning the+-- skolem constants and the skolemised type.+skolemise :: Pos -> Sigma -> TI ([TyVar], Rho)+skolemise pos (TForAll tvs t) = do+ sks1 <- mapM newSkolemTyVar tvs+ let sksTs = map (annotate pos . TVar) sks1+ t <- substType t+ (sks2, t') <- skolemise pos $ substTyVar tvs sksTs t+ return (sks1 ++ sks2, t')+skolemise pos (TFun argT resT) = do+ (sks, resT') <- skolemise pos resT+ return (sks, withAnn pos (TFunF argT resT'))+skolemise _ t =+ return ([], t)++unify :: Type -> Type -> TI ()+unify t1 t2 = do+ s <- gets tiSubst+ u <- mgu (apply s t1) (apply s t2)+ modify (\st -> st { tiSubst = u <> tiSubst st })++mgu :: Type -> Type -> TI Subst+mgu (TFun l r) (TFun l' r') = do+ s1 <- mgu l l'+ s2 <- mgu (apply s1 r) (apply s1 r')+ return $ s2 <> s1+mgu (TMetaVar u) t@(TMetaVar v) = unifyConstraints (getAnn t) u v+mgu l@(TMetaVar v) t = varBind (getAnn l) v t+mgu t r@(TMetaVar v) = varBind (getAnn r) v t+mgu (TVar u) (TVar v)+ | u == v = return nullSubst+mgu TInt TInt = return nullSubst+mgu TDbl TDbl = return nullSubst+mgu TBool TBool = return nullSubst+mgu TChar TChar = return nullSubst+mgu TText TText = return nullSubst+mgu (TList u) (TList v) = mgu u v+mgu (TRecord row1) (TRecord row2) = mgu row1 row2+mgu (TVariant row1) (TVariant row2) = mgu row1 row2+mgu TRowEmpty TRowEmpty = return nullSubst+mgu row1@TRowExtend{} row2@TRowEmpty = unifyRow row1 row2+mgu row1@TRowEmpty row2@TRowExtend{} = unifyRow row2 row1+mgu row1@TRowExtend{} row2@TRowExtend{} = unifyRow row1 row2+mgu t1 t2 = throwError'+ [ "Types do not unify:"+ , ppPos (getAnn t1) <+> ":" <+> ppType t1+ , ppPos (getAnn t2) <+> ":" <+> ppType t2+ ]++unifyRow :: Type -> Type -> TI Subst+unifyRow row1@TRowExtend{} row2@TRowEmpty = throwError' $+ [ ppPos (getAnn row1) <+> ": cannot insert the label(s)"+ <+> hcat (L.intersperse comma (map text . M.keys . rowToMap $ row1))+ , "into row introduced at" <+> ppPos (getAnn row2)+ ]+unifyRow row1@(TRowExtend label1 fieldTy1 rowTail1) row2@TRowExtend{} = do+ -- apply side-condition to ensure termination+ (fieldTy2, rowTail2, theta1) <- rewriteRow (getAnn row1) (getAnn row2) row2 label1+ case snd (toList rowTail1) >>= extractMetaTv of+ Just tv | isInSubst tv theta1 ->+ throwError $ show (getAnn row1) ++ " : recursive row type"+ _ -> do+ theta2 <- mgu (apply theta1 fieldTy1) (apply theta1 fieldTy2)+ let s = theta2 <> theta1+ theta3 <- mgu (apply s rowTail1) (apply s rowTail2)+ return $ theta3 <> s+unifyRow t1 t2 = error $ "Assertion failed: " ++ show (t1, t2)++-- | in order to unify two meta type variables, we must unify any constraints+unifyConstraints :: Pos -> MetaTv -> MetaTv -> TI Subst+unifyConstraints pos u v+ | u == v = return nullSubst+ | otherwise =+ case (metaConstraint u, metaConstraint v) of+ (CNone, CNone) ->+ return $ u |-> annotate pos (TMetaVar v)+ (c1, c2) -> do+ let prefix = metaPrefix v+ w <- newMetaVar pos (c1 `unionConstraints` c2) prefix+ return $ mconcat+ [ u |-> w+ , v |-> w+ ]++varBind :: Pos -> MetaTv -> Type -> TI Subst+varBind pos u t+ | u `S.member` meta t = throwError'+ [ "Occur check fails:"+ , ppPos pos <+> ppType (TMetaVar u)+ , "occurs in"+ , ppPos (getAnn t) <+> ppType t+ ]+ | otherwise =+ case metaConstraint u of+ CNone -> return $ u |-> t+ CStar c+ | t `satisfies` metaConstraint u -> return $ u |-> t+ | otherwise ->+ throwError'+ [ "The type:"+ , ppPos (getAnn t) <+> ":" <+> ppType t+ , "does not satisfy the constraint:"+ , ppPos pos <+> ":" <+> ppStarConstraint c+ ]+ CRow{} -> varBindRow (getAnn t) u t++-- | bind the row tyvar to the row type, as long as the row type does not+-- contain the labels in the tyvar lacks constraint; and propagate these+-- label constraints to the row variable in the row tail, if there is one.+varBindRow :: Pos -> MetaTv -> Type -> TI Subst+varBindRow pos u t+ = case S.toList (ls `S.intersection` ls') of+ [] | Nothing <- mv -> return s1+ | Just r1 <- mv -> do+ let c = ls `S.union` (labelsFrom r1)+ r2 <- newMetaVar pos (CRow c) 'r'+ let s2 = r1 |-> r2+ return $ s1 <> s2+ labels -> throwError $ show $+ ppPos pos <+> ": repeated label(s):"+ <+> sepBy comma (map text labels)+ where+ ls = labelsFrom u+ (ls', mv) = (S.fromList . map fst) *** (>>= extractMetaTv) $ toList t+ s1 = u |-> t+ labelsFrom v = case metaConstraint v of+ CRow s -> s+ _ -> S.empty++rewriteRow :: Pos -> Pos -> Type -> Label -> TI (Type, Type, Subst)+rewriteRow pos1 pos2 (Fix (TRowEmptyF :*: _)) newLabel =+ throwError $ show $+ ppPos pos1 <+> ": label" <+> text newLabel <+> "cannot be inserted into row type introduced at" <+> ppPos pos2+rewriteRow pos1 pos2 (Fix (TRowExtendF label fieldTy rowTail :*: K pos)) newLabel+ | newLabel == label =+ -- nothing to do+ return (fieldTy, rowTail, nullSubst)+ | TVar v <- rowTail, tyvarFlavour v == Skolem =+ throwError $ show $ vcat $+ [ ppPos pos1 <+> ": Type not polymorphic enough:"+ , ppPos pos2+ ]+ | TMetaVar alpha <- rowTail = do+ beta <- newMetaVar pos (lacks [newLabel]) 'r'+ gamma <- newMetaVar pos CNone 'a'+ s <- varBindRow pos alpha+ $ withAnn pos+ $ TRowExtendF newLabel gamma beta+ return ( gamma+ , apply s $ withAnn pos $ TRowExtendF label fieldTy beta+ , s+ )+ | otherwise = do+ (fieldTy', rowTail', s) <- rewriteRow pos1 pos2 rowTail newLabel+ return (fieldTy', TRowExtend label fieldTy rowTail', s)+rewriteRow _ _ ty _ = error $ "Unexpected type: " ++ show ty++-- | type-checking and inference+tcRho :: Exp -> Maybe Rho -> TI Type+tcRho = cata alg+ where+ alg :: (ExpF Name Bind Type :*: K Pos) (Maybe Rho -> TI Type)+ -> Maybe Rho+ -> TI Type+ alg (EVar n :*: K pos) mty = do+ sigma <- lookupVar pos n+ instSigma pos sigma mty+ alg (EPrim prim :*: K pos) mty = do+ let sigma = tcPrim pos prim+ instSigma pos sigma mty+ alg (ELam b e :*: K pos) Nothing = do -- TODO see Mu tCheckPats?+ varT <- newMetaVar pos CNone 'a'+ binds <- tcBinds pos b $ Just varT+ extendEnv binds $ do+ resT <- e Nothing+ return $ withAnn pos $ TFunF varT resT+ alg (ELam b e :*: K pos) (Just ty) = do+ (varT, bodyT) <- unifyFun pos ty+ binds <- tcBinds pos b $ Just varT+ extendEnv binds $+ e (Just bodyT)+ alg (EAnnLam b argT e :*: K pos) Nothing = do+ argT <- instWildcards argT+ binds <- tcBinds pos b $ Just argT+ extendEnv binds $ do+ resT <- e Nothing+ return $ withAnn pos $ TFunF argT resT+ alg (EAnnLam b varT e :*: K pos) (Just ty) = do+ varT <- instWildcards varT+ (argT, bodyT) <- unifyFun pos ty+ subsCheck pos argT varT+ binds <- tcBinds pos b $ Just varT+ extendEnv binds $+ e (Just bodyT)+ alg (EApp e1 e2 :*: K pos) mty = do+ funT <- e1 Nothing+ (argT, resT) <- unifyFun pos funT+ checkSigma pos e2 argT+ instSigma pos resT mty+ alg (ELet b e1 e2 :*: K pos) mty = do+ t1 <- e1 Nothing+ binds <- tcBinds pos b (Just t1) >>= mapM (inferSigma pos)+ extendEnv binds $+ e2 mty+ alg (EAnn e annT :*: K pos) mty = do+ annT <- instWildcards annT+ checkSigma pos e annT+ instSigma pos annT mty++inferSigma :: Pos -> Rho -> TI Sigma+inferSigma pos rho = do+ exp_ty <- substType rho+ env_tys <- getEnvTypes+ let env_tvs = meta env_tys+ res_tvs = meta [exp_ty]+ forall_tvs = S.toList $ res_tvs S.\\ env_tvs+ return $ quantify pos forall_tvs exp_ty++checkSigma :: Pos -> (Maybe Rho -> TI Rho) -> Sigma -> TI ()+checkSigma pos e sigma = do+ (skol_tvs, rho) <- skolemise pos sigma+ void $ e (Just rho)+ env_tys <- getEnvTypes+ let esc_tvs = ftv (sigma : env_tys)+ bad_tvs = filter (`S.member` esc_tvs) skol_tvs+ unless (null bad_tvs) $+ throwError'+ [ ppPos pos <+> ": Type not polymorphic enough:"+ , parensList (map (text . tyvarName) bad_tvs)+ ]++instSigma :: Pos -> Sigma -> Maybe Rho -> TI Type+instSigma pos t1 Nothing = instantiate pos t1+instSigma pos t1 (Just t2) = subsCheckRho pos t1 t2 >> return t2++-- NOTE: Currently we support only simple unamed type wildcards.+-- Each one is distinct and we generate fresh meta vars for them.+instWildcards :: Rho -> TI Rho+instWildcards = cataM alg+ where+ alg :: (TypeF :*: K Pos) Type -> TI Type+ alg (TVarF v :*: K pos) | tyvarFlavour v == Wildcard = do+ mv <- newMetaTyVar (tyvarConstraint v) 't'+ return $ withAnn pos (TMetaVarF mv)+ alg e = return $ Fix e++tcBinds :: Pos -> Bind Name -> Maybe Rho -> TI (M.Map Name Type)+tcBinds pos arg Nothing =+ newMetaVar pos CNone 'a' >>= tcBinds pos arg . Just+tcBinds _ (Arg x) (Just ty) =+ return $ M.singleton x ty+tcBinds pos (RecArg xs) (Just ty) = do+ tvs <- mapM (const $ newMetaVar pos CNone 'l') xs+ r <- newMetaVar pos (lacks xs) 'r' -- implicit tail+ unify ty (TRecord $ mkRowType r $ zip xs tvs)+ return $ M.fromList $ zip xs tvs+tcBinds pos RecWildcard (Just ty) = do+ s <- gets tiSubst+ case apply s ty of+ TRecord r -> return $ rowToMap r+ _ ->+ throwError $ show $+ ppPos pos <+> ": record wildcard cannot bind to type:" <+> ppType ty+++subsCheck :: Pos -> Sigma -> Sigma -> TI ()+subsCheck pos sigma1 sigma2 = do+ (skol_tvs, rho2) <- skolemise pos sigma2+ subsCheckRho pos sigma1 rho2+ let esc_tvs = ftv [sigma1, sigma2]+ bad_tvs = filter (`S.member` esc_tvs) skol_tvs+ unless (null bad_tvs) $+ throwError'+ [ ppPos pos <+> ": Subsumption check failed:"+ , indent 2 (ppType sigma1)+ , text "is not as polymorphic as"+ , indent 2 (ppType sigma2)+ ]++subsCheckRho :: Pos -> Sigma -> Rho -> TI ()+subsCheckRho pos sigma1@(TForAll _ _) rho2 = do+ rho1 <- instantiate pos sigma1+ subsCheckRho pos rho1 rho2+subsCheckRho pos rho1 (TFun a2 r2) = do+ (a1, r1) <- unifyFun pos rho1+ subsCheckFun pos a1 r1 a2 r2+subsCheckRho pos (TFun a1 r1) rho2 = do+ (a2, r2) <- unifyFun pos rho2+ subsCheckFun pos a1 r1 a2 r2+subsCheckRho _ tau1 tau2 =+ unify tau1 tau2++subsCheckFun :: Pos -> Sigma -> Rho -> Sigma -> Rho -> TI ()+subsCheckFun pos a1 r1 a2 r2 = do+ subsCheck pos a2 a1+ subsCheckRho pos r1 r2++unifyFun :: Pos -> Rho -> TI (Sigma, Rho)+unifyFun _ (TFun argT resT) = return (argT, resT)+unifyFun pos tau = do+ argT <- newMetaVar pos CNone 'a'+ resT <- newMetaVar pos CNone 'b'+ unify tau (withAnn pos $ TFunF argT resT)+ return (argT, resT)++-- used by the Repl+tcDecl :: Pos -> Bind Name -> Exp -> TI TypeEnv+tcDecl pos b e = do+ t <- tcRho e Nothing+ binds <- tcBinds pos b (Just t) >>= mapM (inferSigma pos)+ extendEnv binds ask++tcPrim :: Pos -> Prim -> Type+tcPrim pos prim = annotate pos $ case prim of+ Int{} -> TInt+ Dbl{} -> TDbl+ Bool{} -> TBool+ Char{} -> TChar+ Text{} -> TText+ Show ->+ -- use an Eq constraint, to prevent attempting to show lambdas+ let a = newTyVar (CStar CEq) 'a'+ in TForAll [a] $ TFun (TVar a) TText+ Trace ->+ let a = newTyVar CNone 'a'+ in TForAll [a] $ TFun (TFun TText (TVar a))+ (TVar a)+ ErrorPrim ->+ let a = newTyVar CNone 'a'+ in TForAll [a] $ TFun TText (TVar a)++ ArithPrim{} ->+ binOp $ newTyVar (CStar CNum) 'a'+ RelPrim{} ->+ binOpB $ newTyVar (CStar COrd) 'a'++ Not -> TFun TBool TBool+ And -> TFun TBool (TFun TBool TBool)+ Or -> TFun TBool (TFun TBool TBool)++ Eq -> binOpB $ newTyVar (CStar CEq) 'a'+ NEq -> binOpB $ newTyVar (CStar CEq) 'a'++ Double -> TFun TInt TDbl+ Floor -> TFun TDbl TInt+ Ceiling -> TFun TDbl TInt+ Abs ->+ unOp $ newTyVar (CStar CNum) 'a'+ Neg ->+ unOp $ newTyVar (CStar CNum) 'a'+ Mod ->+ TFun TInt (TFun TInt TInt)+ FixPrim ->+ let a = newTyVar CNone 'a'+ in TForAll [a] $ TFun (TFun (TVar a) (TVar a)) (TVar a)+ FwdComp -> -- forward composition operator+ let a = newTyVar CNone 'a' -- (a -> b) -> (b -> c) -> a -> c+ b = newTyVar CNone 'b'+ c = newTyVar CNone 'c'+ in TForAll [a,b,c] $ TFun (TFun (TVar a) (TVar b))+ (TFun (TFun (TVar b) (TVar c))+ (TFun (TVar a) (TVar c)))+ BwdComp -> -- backward composition operator+ let a = newTyVar CNone 'a' -- (b -> c) -> (a -> b) -> a -> c+ b = newTyVar CNone 'b'+ c = newTyVar CNone 'c'+ in TForAll [a,b,c] $ TFun (TFun (TVar b) (TVar c))+ (TFun (TFun (TVar a) (TVar b))+ (TFun (TVar a) (TVar c)))+ Pack -> TFun (TList TChar) TText+ Unpack -> TFun TText (TList TChar)+ Cond ->+ let a = newTyVar CNone 'a'+ in TForAll [a] $ TFun TBool+ (TFun (TVar a)+ (TFun (TVar a) (TVar a)))+ ListEmpty ->+ let a = newTyVar CNone 'a'+ in TForAll [a] $ TList (TVar a)+ ListCons ->+ let a = newTyVar CNone 'a'+ in TForAll [a] $ TFun (TVar a)+ (TFun (TList (TVar a))+ (TList (TVar a)))+ ListFoldr ->+ let a = newTyVar CNone 'a'+ b = newTyVar CNone 'b'+ in TForAll [a,b] $ TFun (TFun (TVar a) (TFun (TVar b) (TVar b)))+ (TFun (TVar b)+ (TFun (TList (TVar a))+ (TVar b)))+ ListNull ->+ let a = newTyVar CNone 'a'+ in TForAll [a] $ TFun (TList (TVar a)) TBool+ ListAppend ->+ let a = newTyVar CNone 'a'+ in TForAll [a] $ TFun (TList (TVar a))+ (TFun (TList (TVar a))+ (TList (TVar a))) -- TODO+ RecordEmpty -> TRecord TRowEmpty+ (RecordSelect label) ->+ let a = newTyVar CNone 'a'+ r = newTyVar (lacks [label]) 'r'+ in TForAll [a,r] $+ TFun (TRecord $ TRowExtend label (TVar a) (TVar r)) (TVar a)+ (RecordExtend label) ->+ let a = newTyVar CNone 'a'+ r = newTyVar (lacks [label]) 'r'+ in TForAll [a,r] $+ TFun (TVar a)+ (TFun (TRecord (TVar r))+ (TRecord $ TRowExtend label (TVar a) (TVar r)))+ (RecordRestrict label) ->+ let a = newTyVar CNone 'a'+ r = newTyVar (lacks [label]) 'r'+ in TForAll [a,r] $+ TFun (TRecord $ TRowExtend label (TVar a) (TVar r))+ (TRecord (TVar r))+ Absurd ->+ let a = newTyVar CNone 'a'+ in TForAll [a] $ TFun (TVariant TRowEmpty) (TVar a)+ (VariantInject label) -> -- dual of record select+ let a = newTyVar CNone 'a'+ r = newTyVar (lacks [label]) 'r'+ in TForAll [a, r] $+ TFun (TVar a)+ (TVariant $ TRowExtend label (TVar a) (TVar r))+ -- a -> <l:a|r>+ (VariantEmbed label) -> -- dual of record restrict+ let a = newTyVar CNone 'a'+ r = newTyVar (lacks [label]) 'r'+ in TForAll [a, r] $+ TFun (TVariant (TVar r))+ (TVariant $ TRowExtend label (TVar a) (TVar r))+ -- <r> -> <l:a|r>+ (VariantElim label) ->+ let a = newTyVar CNone 'a'+ b = newTyVar CNone 'b'+ r = newTyVar (lacks [label]) 'r'+ in TForAll [a, b, r] $+ TFun (TFun (TVar a) (TVar b))+ (TFun (TFun (TVariant (TVar r)) (TVar b))+ (TFun (TVariant $ TRowExtend label (TVar a) (TVar r))+ (TVar b)))+ -- (a -> b) -> (<r> -> b) -> <l:a|r> -> b++ where+ binOpB tv = TForAll [tv] $ TFun ty (TFun ty TBool)+ where ty = TVar tv+ binOp tv = TForAll [tv] $ TFun ty (TFun ty ty)+ where ty = TVar tv+ unOp tv = TForAll [tv] $ TFun ty ty+ where ty = TVar tv++throwError' :: [Doc] -> TI a+throwError' = throwError . show . vcat
+ src/Expresso/Utils.hs view
@@ -0,0 +1,124 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++-- |+-- Module : Expresso.Utils+-- Copyright : (c) Tim Williams 2017-2019+-- License : BSD3+--+-- Maintainer : info@timphilipwilliams.com+-- Stability : experimental+-- Portability : portable+--+-- Recursion scheme utilities.+--+module Expresso.Utils(+ Fix(..),+ K(..),+ (:*:)(..),+ (:+:)(..),+ cata,+ cataM,+ para,+ ana,+ (&&&),+ (***),+ first,+ second,+ showError,+ View(..),+ annotate,+ stripAnn,+ getAnn,+ withAnn+)+where++import Control.Monad+import Data.Data++newtype Fix f = Fix { unFix :: f (Fix f) }++deriving instance (Typeable f, Data (f (Fix f))) => Data (Fix f)++data K a b = K { unK :: a }+ deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Data)++data (f :*: g) a = (:*:) { left :: f a, right :: g a }+ deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Data)++data (f :+: g) a = InL (f a) | InR (g a)+ deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Data)++cata :: Functor f => (f a -> a) -> Fix f -> a+cata phi = phi . fmap (cata phi) . unFix++cataM :: (Monad m, Traversable f) =>+ (f a -> m a) -> Fix f -> m a+cataM algM = algM <=< (mapM (cataM algM) . unFix)++para :: Functor f => (f (b, Fix f) -> b) -> Fix f -> b+para phi = phi . fmap (para phi &&& id) . unFix++ana :: Functor f => (a -> f a) -> a -> Fix f+ana coalg = Fix . fmap (ana coalg) . coalg++-- Equivalent to specialized version from Arrow+(&&&) :: (a -> b) -> (a -> c) -> (a -> (b,c))+f &&& g = \a -> (f a, g a)++-- Equivalent to specialized version from Arrow+(***) :: (a -> b) -> (c -> d) -> ((a, c) -> (b, d))+f *** g = \(a, b) -> (f a, g b)++-- Equivalent to specialized version from Arrow+first :: (a -> b) -> (a,c) -> (b,c)+first f (a,c) = (f a, c)++-- Equivalent to specialized version from Arrow+second :: (b -> c) -> (a,b) -> (a,c)+second f (a,b) = (a, f b)++instance (Functor f, Show (f (Fix f))) => Show (Fix f) where+ showsPrec d (Fix f) = showsPrec d f++instance (Functor f, Eq (f (Fix f))) => Eq (Fix f) where+ fa == fb = unFix fa == unFix fb++instance (Functor f, Ord (f (Fix f))) => Ord (Fix f) where+ compare fa fb = compare (unFix fa) (unFix fb)++class View f a where+ proj :: a -> f a+ inj :: f a -> a++showError :: Show a => Either a b -> Either String b+showError = either (Left . show) Right++-- | add annotation+annotate :: forall f a. Functor f => a -> Fix f -> Fix (f :*: K a)+annotate ann = cata alg where+ alg :: f (Fix (f :*: K a)) -> Fix (f :*: K a)+ alg e = Fix (e :*: K ann)++-- | strip annotations+stripAnn :: forall f a. Functor f => Fix (f :*: K a) -> Fix f+stripAnn = cata alg where+ alg :: (f :*: K a) (Fix f) -> Fix f+ alg (e :*: _) = Fix e++-- | retrieve annotation+getAnn :: Fix (f :*: K a) -> a+getAnn = unK . right . unFix++-- | fix with annotation+withAnn :: a -> f (Fix (f :*: K a) )-> Fix (f :*: K a)+withAnn ann e = Fix (e :*: K ann)
+ src/Repl.hs view
@@ -0,0 +1,247 @@+{-# LANGUAGE ScopedTypeVariables #-}++-- |+-- Module : Main+-- Copyright : (c) Tim Williams 2017-2019+-- License : BSD3+--+-- Maintainer : info@timphilipwilliams.com+-- Stability : experimental+-- Portability : portable+--+-- Expresso Read-Eval-Print-Loop.+--+module Main where++import Control.Applicative+import Control.Monad (forM_)+import Control.Monad.IO.Class+import Control.Monad.State.Strict+import Data.Char+import System.Console.Haskeline (InputT)+import System.Console.Haskeline.MonadException ()+import System.Directory+import System.FilePath+import Text.Parsec.String (Parser)+import qualified System.Console.Haskeline as HL+import qualified Text.Parsec as P++import Expresso+import Expresso.Parser ( pExp, pLetDecl, topLevel+ , reserved, reservedOp, stringLiteral+ )+import Expresso.Utils++ps1 :: String+ps1 = "λ"++data Mode = SingleLine | MultiLine | Quitting++data ReplState = ReplState+ { stateMode :: Mode+ , stateBuffer :: [String]+ , stateEnv :: Environments+ }++data Command+ = Peek ExpI+ | Type ExpI+ | ChangeCWD FilePath+ | BeginMulti+ | Reset+ | DumpEnv+ | Quit+ | Help++data Line+ = Command Command+ | Term ExpI+ | Decl (Bind Name) ExpI+ | NoOp++type Repl = InputT (StateT ReplState IO)++main :: IO ()+main = do+ cwd <- liftIO getCurrentDirectory+ let preludePath = cwd </> "Prelude.x"+ runRepl $ do+ mapM_ spew+ [ "Expresso REPL"+ , "Type :help or :h for a list of commands"+ ]+ HL.catch+ (loadPrelude preludePath)+ (\(e :: HL.SomeException) ->+ spew $ "Warning: Couldn't open " ++ preludePath ++ ": " ++ show e)+ repl++-- | The read-eval-print-loop+repl :: Repl ()+repl = step repl+ `HL.catch` (\(e :: HL.SomeException) -> spew (show e) >> repl)+ where+ step :: Repl () -> Repl ()+ step cont = HL.withInterrupt $ do+ mode <- lift $ gets stateMode+ case mode of+ MultiLine -> do+ minput <- HL.getInputLine $ ps1 ++ "| "+ whenJust minput $ \input ->+ if isEndMulti input+ then doEndMulti+ else lift $ modify (addToBuffer input)+ cont+ SingleLine -> do+ minput <- HL.getInputLine $ ps1 ++ "> "+ whenJust minput process+ cont+ Quitting -> do+ spew "Goodbye."+ return ()++process :: String -> Repl ()+process str = do+ case parseLine str of+ Left err -> spew err+ Right (Command c) -> doCommand c+ Right (Term e) -> doEval showValue' e+ Right (Decl b e) -> doDecl b e+ Right NoOp -> return ()+ `HL.catch` handler+ where+ handler :: HL.SomeException -> Repl ()+ handler ex = spew $ "Caught exception: " ++ show ex++runRepl :: Repl a -> IO a+runRepl m = do+ historyFile <- (</> ".expresso_history") <$> getHomeDirectory+ let settings = HL.defaultSettings {HL.historyFile = Just historyFile}+ evalStateT (HL.runInputT settings m) emptyReplState++emptyReplState :: ReplState+emptyReplState = ReplState+ { stateMode = SingleLine+ , stateBuffer = mempty+ , stateEnv = initEnvironments+ }++loadPrelude :: FilePath -> Repl ()+loadPrelude path = do+ doDecl RecWildcard $ Fix (InR (K (Import path)) :*: K dummyPos)+ spew $ "Loaded Prelude from " ++ path++doCommand :: Command -> Repl ()+doCommand c = case c of+ Peek e -> doEval (return . showValue) e+ Type e -> doTypeOf e+ ChangeCWD path -> liftIO $ setCurrentDirectory path+ Quit -> lift $ modify (setMode Quitting)+ BeginMulti -> lift $ modify (setMode MultiLine)+ Reset -> doReset+ DumpEnv -> doDumpEnv+ Help -> mapM_ spew+ [ "REPL commands available from the prompt:"+ , ""+ , "<expression> evaluate an expression"+ , ":peek <expression> evaluate, but not deeply"+ , ":{\\n ..lines.. \\n:}\\n multiline command"+ , ":cd <path> change current working directory"+ , ":type <term> show the type of <term>"+ , ":reset reset REPL, unloading all definitions"+ , ":env dump bound symbols in the environment"+ , ":quit exit REPL"+ , ":help display this list of commands"+ , ""+ ]++doEval :: (Value -> IO String) -> ExpI -> Repl ()+doEval pp e = do+ envs <- lift $ gets stateEnv+ v'e <- liftIO $ evalWithEnv envs e+ case v'e of+ Left err -> spew err+ Right val -> liftIO (pp val) >>= spew++doDecl :: Bind Name -> ExpI -> Repl ()+doDecl b e = do+ envs <- lift $ gets stateEnv+ envs'e <- liftIO $ runEvalM $ bind envs b e+ case envs'e of+ Left err -> spew err+ Right envs' -> lift $ modify (setEnv envs')++doTypeOf :: ExpI -> Repl ()+doTypeOf e = do+ envs <- lift $ gets stateEnv+ ms <- liftIO $ typeOfWithEnv envs e+ case ms of+ Left err -> spew err+ Right sigma -> spew (showType sigma)++doReset :: Repl ()+doReset = lift $ modify (setEnv $ stateEnv emptyReplState)++doDumpEnv :: Repl ()+doDumpEnv = do+ envs <- lift $ gets stateEnv+ forM_ (dumpTypeEnv envs) $ \(name, sigma) ->+ spew $ name ++ " : " ++ showType sigma++parseLine :: String -> Either String Line+parseLine str+ | all isSpace str = return NoOp+ | otherwise = showError $ P.parse (topLevel pLine) "<interactive>" str++pLine :: Parser Line+pLine = pCommand <|> P.try pTerm <|> pDecl++pTerm :: Parser Line+pTerm = Term <$> pExp++pDecl :: Parser Line+pDecl = uncurry Decl <$> (reserved "let" *> pLetDecl)++pCommand :: Parser Line+pCommand = Command <$> (reservedOp ":" *> p)+ where+ p = (reserved "peek" <|> reserved "p") *> (Peek <$> pExp)+ <|> (reserved "type" <|> reserved "t") *> (Type <$> pExp)+ <|> reserved "cd" *> (ChangeCWD <$> pFilePath)+ <|> (reserved "reset" <|> reserved "r") *> pure Reset+ <|> (reserved "env" <|> reserved "e") *> pure DumpEnv+ <|> (reserved "quit" <|> reserved "q") *> pure Quit+ <|> (reserved "help"+ <|> reserved "h" <|> reserved "?") *> pure Help+ <|> reserved "{" *> pure BeginMulti++pFilePath :: Parser FilePath+pFilePath = stringLiteral -- TODO++setMode :: Mode -> ReplState -> ReplState+setMode m s = s { stateMode = m }++setEnv :: Environments -> ReplState -> ReplState+setEnv envs s = s { stateEnv = envs }++addToBuffer :: String -> ReplState -> ReplState+addToBuffer str s = s { stateBuffer = stateBuffer s ++ [str] }++doEndMulti :: Repl ()+doEndMulti = do+ str <- lift $ gets (unlines . stateBuffer)+ lift $ modify $ clearBuffer . setMode SingleLine+ process str++clearBuffer :: ReplState -> ReplState+clearBuffer s = s { stateBuffer = mempty }++isEndMulti :: String -> Bool+isEndMulti ":}" = True+isEndMulti _ = False++spew :: String -> Repl ()+spew = HL.outputStrLn++whenJust :: Applicative m => Maybe a -> (a -> m ()) -> m ()+whenJust mg f = maybe (pure ()) f mg
+ src/Tests.hs view
@@ -0,0 +1,173 @@+module Main where++import Test.Tasty (TestTree, defaultMain, testGroup)+import Test.Tasty.HUnit (assertEqual, assertFailure, testCase)+import Data.HashMap.Strict (HashMap)+import qualified Data.HashMap.Strict as HashMap++import Expresso++main = defaultMain unitTests++unitTests = testGroup+ "End-to-end functional tests"+ [ letTests+ , lambdaTests+ , recordTests+ , variantTests+ , listTests+ , relationalTests+ , inferenceTests+ , constraintTests+ , rankNTests+ , lazyTests+ ]++letTests = testGroup+ "Let expressions"+ [ hasValue "let x = 1 in x" (1::Integer)+ , hasValue "let x = 1 in let y = 2 in x + y" (3::Integer)+ , hasValue "let x = 1; y = 2 in x + y" (3::Integer)+ , hasValue "let {..} = {inc = x -> x + 1} in inc 1" (2::Integer)+ , hasValue "let m = {inc = x -> x + 1} in m.inc 1" (2::Integer)++ , hasValue "let m = {id = x -> x} in {foo = [m.id 1], bar = m.id [1]}"+ ["foo" --> ([1]::[Integer]), "bar" --> ([1]::[Integer])]++ -- Record argument field-pun generalisation+ , hasValue "let {id} = {id = x -> x} in {foo = [id 1], bar = id [1]}"+ ["foo" --> ([1]::[Integer]), "bar" --> ([1]::[Integer])]+ , hasValue "let {..} = {id = x -> x} in {foo = [id 1], bar = id [1]}"+ ["foo" --> ([1]::[Integer]), "bar" --> ([1]::[Integer])]++ -- Num constraint violation+ , illTyped "let square = x -> x * x in {foo = square 1, bar = square [1]}"+ ]++lambdaTests = testGroup+ "Lambda expressions"+ [ hasValue "(x -> y -> x + y) 1 2" (3::Integer)+ , hasValue "(x y -> x + y) 1 2" (3::Integer)+ , illTyped "x -> x x"+ , illTyped "let absorb = fix (r x -> r) in absorb"+ , illTyped "let create = fix (r x -> r x x) in create"+ ]++recordTests = testGroup+ "Record expressions"+ [ hasValue "({x, y} -> {x, y}) {x=1, y=2}" $ toMap ["x"-->(1::Integer), "y"-->2]+ , hasValue "{x = 1, y = 2}" $ toMap ["x"-->(1::Integer), "y"-->2]+ , hasValue "(r -> { x = 1, y = 2 | r}) { z = 3 }" $ toMap ["x"-->(1::Integer), "y"-->2, "z"-->3]+ , hasValue "{ x = { y = { z = 42 }}}.x.y.z" (42::Integer)++ -- Row tail unification soundness+ , illTyped "r -> if True then { x = 1 | r } else { y = 2 | r }"++ , illTyped "{ x = 2, x = 1 }.x" -- fails to typecheck+ , illTyped "{ x = 2 | { x = 1 }}.x" -- fails to typecheck+ , hasValue "{ x := 2, x = 1 }.x" (2::Integer)+ , hasValue "{ x := 2 | { x = 1 }}.x" (2::Integer)+ , hasValue "{| x = 1 |} {}" $ toMap ["x"-->(1::Integer)]+ , hasValue "({| x = 1, y = 2 |} >> {| z = 3 |}) {}" $ toMap ["x"-->(1::Integer), "y"-->2, "z"-->3]+ , hasValue "({| x = 1, y = 2 |} >> {| x := 42 |}) {}" $ toMap ["x"-->(42::Integer), "y"-->2]+ , illTyped "({| x = 1, y = 2 |} << {| x := 42 |}) {}" -- fails to typecheck+ , hasValue "({| x := 42, y = 2 |} << {| x = 1 |}) {}" ["x"-->(42::Integer), "y"-->2]+ ]++variantTests = testGroup+ "Variant expressions"+ [ hasValue "case Foo 1 of { Foo x -> x + 1, Bar {x, y} -> x + y }" (2::Integer)+ , hasValue "case Bar {x=1, y=2} of { Foo x -> x + 1, Bar {x, y} -> x + y }" (3::Integer)+ , illTyped "case Baz{} of { Foo x -> x + 1, Bar {x, y} -> x + y }" -- fails to typecheck+ , hasValue "case Baz{} of { Foo x -> x + 1, Bar {x, y} -> x + y | otherwise -> 42 }" (42::Integer)+ , illTyped "let f = s -> case s of { Foo x -> x + 1, Bar {x, y} -> x + y }; g = s -> f (<|Foo|> s) in g (Foo 1)" -- fails to typecheck+ , hasValue "let f = s -> case s of { Foo x -> x + 1, Bar {x, y} -> x + y }; g = s -> f (<|Foo|> s) in g (Bar{x=1, y=2})" (3::Integer)+ , hasValue "let f = s -> case s of { Foo x -> x + 1, Bar {x, y} -> x + y | otherwise -> 42 }; g = s -> f (<|Foo,Bar|> s) in g (Baz{})" (42::Integer)+ , hasValue "case Foo 1 of { override Foo x -> x + 2 | s -> case s of { Foo x -> x + 1 }}" (3::Integer)+ , hasValue "case Foo 1 of { override Foo x -> x + 2, Foo x -> x + 1 }" (3::Integer)++ -- Fail in empty row case+ , illTyped "x -> case x of { A{} -> 1, B{} -> 2, A{} -> 3 }"+ -- Fail in row var case+ , illTyped "x -> <|A, B, A|> x"+ -- Failed row rewrite due to row constraints+ , illTyped ("let f = x -> case (<|A|> x) of { B{} -> 1, otherwise -> 2 }; " +++ "let g = x -> case (<|B|> x) of { A{} -> 1, otherwise -> 2 } in " +++ "x -> f x + f x")+ ]++listTests = testGroup+ "List expressions"+ [ hasValue "[1,2,3]" [1::Integer,2,3]+ , illTyped "[1,True]"+ ]++relationalTests = testGroup+ "Relational expressions"+ [ hasValue "(1 == 2)" False+ , hasValue "1/=2" True+ , illTyped "1 == 2 == 3"+ , hasValue "{x = 1, y = True} == {y = True, x = 1}" True -- field order should not matter+ , illTyped "{x = 1, y = True} > {y = True, x = 1}" -- cannot compare records for ordering+ , hasValue "Just 1 == Just 1" True -- variants can be compared for equality+ , illTyped "Foo 1 > Bar{}" -- cannot compare variants for ordering+ , hasValue "[1,2,3] == [1,2,3]" True -- lists can be compared for equality+ , hasValue "[1,2,3] >= [1,2,2]" True -- lists can be compared for ordering+ , hasValue "True&&True" True+ , hasValue "True||False" True+ ]++inferenceTests = testGroup+ "Type inference tests"+ [ hasType "n d -> if d == 0 then DivBy0 {} else Ok (n / d)"+ "forall r. (r\\DivBy0\\Ok) => Int -> Int -> <DivBy0 : {}, Ok : Int | r>"+ ]++constraintTests = testGroup+ "Constraint violations"+ [ illTyped "show { x = \"test\", y = Just (x -> x) }"+ , illTyped "{ x = 2 } > { x = 1}"+ , illTyped "let f = x y -> x + y in f True False"+ ]++rankNTests = testGroup+ "Rank-N polymorphism"+ [ hasValue "let f = (g : forall a. a -> a) -> {l = g True, r = g 1} in f (x -> x) == {l = True, r = 1}" True+ , hasValue "let f = g -> {l = g True, r = g 1} : (forall a. a -> a) -> {l : Bool, r : Int } in f (x -> x) == {l = True, r = 1}" True , hasValue "let f = (m : forall a. { reverse : [a] -> [a] |_}) -> {l = m.reverse [True, False], r = pack (m.reverse (unpack \"abc\")) } in f (import \"Prelude.x\") == {l = [False, True], r = \"cba\"}" True+ ]++lazyTests = testGroup+ "Lazy evaluation tests using error primitive"+ [ -- hasValue "maybe (error \"bang!\") (x -> x == 42) (Just 42)" True+ hasValue "{ x = error \"boom!\", y = 42 }.y" (42::Integer)+ , hasValue "case Bar (error \"fizzle!\") of { Foo{} -> 0 | otherwise -> 42 }" (42::Integer)+ ]++hasValue :: (Eq a, Show a, HasValue a) => String -> a -> TestTree+hasValue str expected = testCase str $ do+ result <- evalString Nothing str+ case result of+ Left err -> assertFailure err+ Right actual -> assertEqual "" expected actual++hasType :: String -> String -> TestTree+hasType str expected = testCase str $ do+ result <- typeOfString str+ case result of+ Left err -> assertFailure err+ Right actual -> assertEqual "" expected (showType actual)++illTyped :: String -> TestTree+illTyped str = testCase str $ do+ sch'e <- typeOfString str+ case sch'e of+ Left _ -> assertTrue+ Right sch -> assertFailure $ "Should not type-check, but got: " ++ showType sch++assertTrue = return ()++(-->) :: HasValue a => Name -> a -> (Name, a)+(-->) l v = (l, v)++toMap :: (Eq a, Show a, HasValue a) => [(Name, a)] -> HashMap Name a+toMap = HashMap.fromList