typerbole (empty) → 0.0.0.1
raw patch · 23 files changed
+2755/−0 lines, 23 filesdep +QuickCheckdep +basedep +bifunctorssetup-changedbinary-added
Dependencies added: QuickCheck, base, bifunctors, checkers, colour, containers, data-ordlist, diagrams-lib, diagrams-svg, either, fgl, generic-random, hspec, lens, megaparsec, mtl, safe, semigroups, syb, template-haskell, th-lift, typerbole
Files
- CONTRIBUTING.md +53/−0
- LICENSE +30/−0
- README.md +85/−0
- Setup.hs +2/−0
- diagrams/Main.hs +13/−0
- diagrams/typeclass-hierarchy.png binary
- lambdacube-overview.md +102/−0
- src/Calculi/Lambda.hs +144/−0
- src/Calculi/Lambda/Cube.hs +9/−0
- src/Calculi/Lambda/Cube/Dependent.hs +21/−0
- src/Calculi/Lambda/Cube/HigherOrder.hs +64/−0
- src/Calculi/Lambda/Cube/Polymorphic.hs +299/−0
- src/Calculi/Lambda/Cube/Polymorphic/Unification.hs +422/−0
- src/Calculi/Lambda/Cube/SimpleType.hs +200/−0
- src/Calculi/Lambda/Cube/TH.hs +169/−0
- src/Compiler/Typesystem/Hask.hs +52/−0
- src/Compiler/Typesystem/SimplyTyped.hs +131/−0
- src/Compiler/Typesystem/SystemF.hs +248/−0
- src/Compiler/Typesystem/SystemFOmega.hs +155/−0
- src/Control/Typecheckable.hs +148/−0
- src/Data/Graph/Inductive/Helper.hs +126/−0
- test/Spec.hs +173/−0
- typerbole.cabal +109/−0
+ CONTRIBUTING.md view
@@ -0,0 +1,53 @@+# Maintainance and Contribution++## Deep-seated problems++This library was developed by me (@Lokidottir, at time of writing) while I was learning type theory as a personal project, in fairly deep isolation from anyone who had already studied it. There's a good chance my assumptions about what things mean conflicts with the literature, I would apprecite any issues or pull requests made pointing out or addressing issues related to this.++Additionally, this library uses an extensive number of GHC extensions. While this has made this project as flexible as it is, it also means that compile times are awful and that some ideas such as Type Families or even just the appearence of `forall`s may not be familiar to people who have learnt plain Haskell2010.++## Style++### Influence++This library was influenced by [Subhask](https://github.com/mikeizbicki/subhask), though using it is avoided in this project for the sake of not making the library more complex than it already is.++### Comments++There's no such thing as self-documenting code or too many comments. Code like below should be avoided, even if it's "obvious" what's going on.++```haskell+{-| ... <docs> ... -}+(⊑) :: (Polymorphic t) => t -> t -> Bool+t ⊑ t' = fromRight False $ do+ subs <- resolveMutuals <$> substitutionsM t' t+ applySubs <- applyAllSubsGr subs+ return (t' ≣ applySubs t)+```++The code below is better, if a bit much. This level of explaination is usually only needed in important functions with fine details, it's appreciated though.++```haskell+{-| ... <docs> ... -}+(⊑) :: (Polymorphic t) => t -> t -> Bool+t ⊑ t' =+ -- if we get a Left value then return false, the type expressions are+ -- incompatable and ordering isn't even a possibility.+ fromRight False $ do+ -- Get the substitution from both types then resolve their mutual+ -- substitutions+ subs <- resolveMutuals <$> substitutionsM t' t+ -- Make a function that applies all substitutions between t and t' to a+ -- given type expression.+ applySubs <- applyAllSubsGr subs+ -- Test if t with all substitutions applied to it is equivalent to t'.+ return (t' ≣ applySubs t)+```++## Contribution++### New typesystems++Introducing new typesystem instances under `Compiler.Typesystem` is welcomed.++### Utility
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Fionan Haralddottir (c) 2016++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * 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.++ * Neither the name of Fionan Haralddottir nor the names of other+ 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+OWNER 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.
+ README.md view
@@ -0,0 +1,85 @@+# typerbole++Parameterized typesystems, lambda cube typeclasses, and typechecking interfaces.++## Parameterized Typesystems++Like how datatypes such as `List a` (`[a]`), `Set a`, `Tree a` etc. in haskell have a parameter for a contained type, this library is based on the idea that a datatype that represents expressions can have a parameter for a typesystem.++### An Example: The Lambda Calculus++As an example, we can put together a datatype that represents the syntax for the Lambda Calculus:++```haskell+data LambdaTerm c v t =+ Variable v -- a variable bound by a lambda abstraction+ | Constant c -- a constant defined outside of the term+ | Apply (LambdaTerm c v t) (LambdaTerm c v t) -- an application of one term to another+ | Lambda (v, t) (LambdaTerm c v t) -- A lambda abstraction+```++This datatype has 3 parameters. The first two parameters represent constants and variables respectively, what's important is the final parameter `t` which is the parameter for the typesystem being used.++We can use the typesystem `SimplyTyped` in `Compiler.Typesystem.SimplyTyped` as the typesystem to make this a simply-typed lambda calculus, or we could slot in `SystemF`, `SystemFOmega`, `Hask`, to change the typesystem associcated with with it.++Sadly there's no magic that builds typecheckers for these (yet). Instead, using the language extensions `MultiParamTypeClasses` and `FlexibleInstances` and the `Typecheckable` typeclass from `Control.Typecheckable` we write a typechecker for each of these occurences.++```haskell+instance (...) => Typecheckable (LambdaTerm c v) (SimplyTyped m) where+ ...+instance (...) => Typecheckable (LambdaTerm c v) (SystemF m p) where+ ...+instance (...) => Typecheckable (LambdaTerm c v) (SystemFOmega m p k) where+ ...+-- and so on.+```++Or we can just ignore it all and turn it into an untyped lambda calculus:++```haskell+type UntypedLambdaTerm c v = LambdaTerm c v ()+```++## The Lambda Cube++The lambda cube describes the properties of a number of typesystems, an overview can be found [**here**](./lambdacube-overview.md). It is the basis for the library's classification of typesystems, a typeclass hierarchy where each axis is represented by a typeclass whose methods and associated types are indicitive of the properties of the axis.++++***++### Supported lambda-cube axies++- [x] Simply-typed lambda calculus+- [x] Polymorphic lambda calculus+- [x] Higher-order lambda calculus+- [x] Dependently-typed lambda calculus (dubiously, not got a implemented typesystem to back it up)++### TODOs++- [ ] Give `Calculi.Lambda.Cube.Polymorphic.Unification` better documentation (incl. diagrams for graph-related functions/anything that'll benefit).+- [ ] Finish the `Typecheckable` & `Inferable` instances for the typesystems in `Compiler.Typesystem.*`+- [ ] Put together a working travis file.+- [ ] Implement a Calculus of Constructions typesystem.+- [ ] Document the type expression psudocode+- [ ] Design a typeclass for typesystems with constraints (`Num a => ...`, `a ~ T` etc).+- [ ] Provide a default way of evaluating lambda expressions.+- [ ] Make the quasiquoters use the lambda cube typeclasses instead of specific typesystem implementations.+- [ ] Subhask-style automated test writing.+- [ ] Explore homotopy type theory+- [ ] Remove all extensions that aren't light syntactic sugar from `default-extensions` and declare them explicitly in the modules they're used.+- [ ] Listen to `-Wall`+- [ ] Move `Control.Typecheckable` to it's own package.+- [ ] Elaborate on the `Typecheck` type. Maybe make it a typeclass.++### Papers, Sites and Books read during development++* Introduction to generalized type systems, Dr Henk Barendregt (Journal of Functional Programming, April 1991)++* A Modern Perspective on Type Theory [(x)](https://www.amazon.co.uk/Modern-Perspective-Type-Theory-Origins/dp/1402023340)++* A proof of correctness for the Hindley-Milner type inference algorithm, Dr Jeff Vaughan [(x)](http://www.jeffvaughan.net/docs/hmproof.pdf)++* Compositional Type Checking for Hindley-Milner Type Systems with Ad-hoc Polymorphism, Dr. Gergő Érdi [(x)](https://gergo.erdi.hu/elte/thesis.pdf)++* Many wikipedia pages on type theory.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ diagrams/Main.hs view
@@ -0,0 +1,13 @@+module Main where++import Diagrams.Prelude+import Diagrams.Backend.SVG.CmdLine+import Data.Colour+import Data.Colour.SRGB++main :: IO ()+main = putStrLn "todo: program making diagrams for this package"++colour = sRGB24++hexcode = sRGB24read
+ diagrams/typeclass-hierarchy.png view
binary file changed (absent → 38416 bytes)
+ lambdacube-overview.md view
@@ -0,0 +1,102 @@+# Overview of Lambda Cube typesystems++## Simply-typed lambda calculus++The simply-typed lambda calculus is *the most simple typesystem* in the lambda cube. It lets you have type constants[1] (`Int`, `Bool`, `String` etc.) and the function arrow `->` to make functions from one type to another.++```haskell+-- Functions and values in the simply-typed lambda calculus.+zero : Int+zero = 0++isFive : Int -> Bool+isFive 5 = True+isFive _ = False++thisFunctionTakesAFunction : (Int -> String) -> String+thisFunctionTakesAFunction f = f 20+```++On it's own, the simply-typed lambda calculus is okay for simple programs. Additionally, if a way to do recursion isn't provided in languages using the STLC then the programs are strongly normalising (they will always terminate).++It's the simplest typesystem in the cube though, there's a low limit to what it can express. Each axis of the lambda cube extends the kind of programs that can be written in a typesafe way.++## Polymorphism++When working in a simply-typed lambda calculus, you can end up writing a lot of duplicate code just because of different types. Like below, an example of writing identity functions for every type (there's an infinite number of them).++```haskell+-- Identity functions in the simply-typed lambda calculus.+identityInt : Int -> Int+identityInt x = x++identityBool : Bool -> Bool+identityBool x = x++identityIntToInt : (Int -> Int) -> (Int -> Int)+identityIntToInt x = x+...+-- Etc. Do for the infinite number of types that exist.+```++Wouldn't it be useful if we could abstract the type away and have a **variable** type that lets us have a single identity function **for all** types like we do for values in the lambda calculus with `\a -> ...`?++So we do just that in the polymorphic lambda calculus, a type variable[2] stands in, able to be replaced by any other type.++```haskell+-- identity function (just the one!) in a polymorphic lambda calculus.+identity : forall a. a -> a+identity x = x+```++And we can use this on all types:++```haskell+-- Ints...+> identity 5+5+-- ...and Strings...+> identity "Type theory is pretty"+"Type theory is pretty"+-- ...and Bools...+> identity False+False+-- ...and functions!+> identity ((\i -> i + 1) : Int -> Int)+(\i -> i + 1) : Int -> Int+```++#### A note on typeclasses++The idea pf typeclass constraints (`Show a => a -> String` and the like) is an extension or syntactic sugar for the polymorphic lambda calculus, and isn't a part of polymorphic lambda calculi by default. They allow a lot more abstraction and generalisation and are not covered in this document.++## Higher-order types++Higher-order types allow for compound types (Like `IO String` or `Set Int` in haskell).++```haskell+listOfInt : [Int]+listOfInt = [1,2,3,4,5]++setOfInt : Set Int+setOfInt = fromList [1,2,3,4,5]+```++## Dependent types++Dependent types let us have values in types at compile time. This can seem confusing, but when using typerbole you are manipulating type expressions as values, this just gives this ability to a programming language targeting a dependent lambda calculus by letting the programmer embed value-level terms at the type level.++<!-- Examples wanted -->++***+##### Footnotes++[1] In typerbole's source code type constants are called mono types because of the lambda calculus implementation uses the names `Variable` and `Constant`.++[2] In typerbole's source type variables are reffered to as poly types, see [1]++***++##### Contribution++This is an educational document, pull requests for better (though accessable) explainations, typos, citations, or signposting to more information for those interested are welcome.
+ src/Calculi/Lambda.hs view
@@ -0,0 +1,144 @@+module Calculi.Lambda (+ -- * Typed Lambda Calculus AST.+ LambdaTerm(..)+ , UntypedLambdaExpr+ -- ** Analysis Helpers+ , freeVars+ -- ** Name-related errors + , NotKnownErr(..)+ -- * Let declaration helpers+ , LetDeclr+ , unlet+ , letsDependency+ , letsDependency'+) where++import Data.Bifunctor.TH+import Data.Either.Combinators+import Data.Either (lefts, partitionEithers)+import Data.Generics (Data(..))+import Data.Graph.Inductive+import Data.Graph.Inductive.Helper+import qualified Data.Map as Map+import Data.Maybe+import Data.Random.Generics+import Data.Semigroup+import qualified Data.Set as Set+import Test.QuickCheck++{-|+ A simple, typed lambda calculus AST with constants.+-}+data LambdaTerm c v t =+ Variable v+ -- ^ A reference to a variable.+ | Constant c+ -- ^ A constant value, such as literals or constructors.+ | Apply (LambdaTerm c v t) (LambdaTerm c v t)+ -- ^ An application of one expression to another.+ | Lambda (v, t) (LambdaTerm c v t)+ -- ^ A lambda expression, with a variable definition and+ -- a function body.+ deriving (Eq, Ord, Show, Data)++deriveBifunctor ''LambdaTerm+deriveBifoldable ''LambdaTerm+deriveBitraversable ''LambdaTerm++instance (Arbitrary c, Data c,+ Arbitrary v, Data v,+ Arbitrary t, Data t) => Arbitrary (LambdaTerm c v t) where+ arbitrary = sized generatorSR++type LetDeclr c v t = ((v, t), LambdaTerm c v t)++type UntypedLambdaExpr c v = LambdaTerm c v ()++{-|+ Name-related errors, for when there's a variable, type or constant+ that doesn't appear in the environment that was given to the typechecker.+-}+data NotKnownErr c v t =+ UnknownType t+ -- ^ A type appears that is not in scope+ | UnknownVariable v+ -- ^ A variable appears that is not in scope+ | UnknownConstant c+ -- ^ A constant appears that is not in scope+ deriving (Eq, Ord, Show)++{-|+ Given the contents of a let expression's declarations, generate a graph+ showing the dependencies between each declaration, including recursion+ as loops.+-}+letsDependency :: (DynGraph gr, Ord c, Ord v, Ord t) => [LetDeclr c v t] -> gr (LetDeclr c v t) ()+letsDependency = snd . letsDependency'++{-|+ `letsDependency` but also return the internally used NodeMap.+-}+letsDependency' :: forall gr c v t. (DynGraph gr, Ord c, Ord v, Ord t)+ => [LetDeclr c v t]+ -> (NodeMap (LetDeclr c v t), gr (LetDeclr c v t) ())+letsDependency' lets =+ let+ declrs = fst . fst <$> lets+ declrsSet = Set.fromList declrs+ -- memoize because we need to check the vars then use the entire declaration and this+ -- is very costly.+ declrMap :: Map.Map v (LetDeclr c v t)+ declrMap = Map.fromList $ zip declrs lets++ {-+ Get the intersection of the free variables in the expression and the set of+ declarations in this let expression.+ -}+ dependsOf :: LetDeclr c v t -> Set.Set v+ dependsOf = Set.intersection declrsSet . freeVars . snd++ {-+ Find all the inward nodes of a declaration.+ -}+ inwardNodes :: LetDeclr c v t -> [LetDeclr c v t]+ inwardNodes declr =+ fromMaybe [] (sequence $ (`Map.lookup` declrMap) <$> Set.toList (dependsOf declr))++ inwardEdges :: LetDeclr c v t -> [(LetDeclr c v t, LetDeclr c v t, ())]+ inwardEdges declr = (\inward -> (inward, declr, ())) <$> inwardNodes declr+ in snd . run empty $ insMapEdgesM (concat $ inwardEdges <$> lets)++{-|+ Unlet non-cyclic let expressions.+-}+unlet :: forall c v t. (Ord c, Ord v, Ord t)+ => [LetDeclr c v t] -- ^ The list of declarations in a let expression+ -> LambdaTerm c v t -- ^ The body of the let declaration+ -> Either [[LetDeclr c v t]]+ (LambdaTerm c v t) -- ^ Either a list of cyclic lets or the final expression+unlet lets expr =+ let -- Build the dependency graph+ depends :: Gr (LetDeclr c v t) () = letsDependency lets+ -- Get the regular topsort.+ tsorted = topsortWithCycles depends+ (cycles, lets') = partitionEithers tsorted+ -- This is what turns the cycles found in tsorted+ -- to let expressions and the non-cycle nodes into+ -- lambda-apply name scoping.+ unlet' (declr, body) lexpr = Lambda declr lexpr `Apply` body+ in if null cycles then Right (foldr unlet' expr lets') else Left cycles++{-|+ Find all the unbound variables in an expression.+-}+freeVars :: Ord v => LambdaTerm c v t -> Set.Set v+freeVars = \case+ Variable v -> Set.singleton v+ Constant _ -> Set.empty+ Apply fun arg ->+ -- Union the free variables of both parts of the Apply+ freeVars fun <> freeVars arg+ Lambda (v, _) expr ->+ -- remove the variable defined by the lambda from the set of free+ -- variables found in the body.+ Set.delete v (freeVars expr)
+ src/Calculi/Lambda/Cube.hs view
@@ -0,0 +1,9 @@+module Calculi.Lambda.Cube (+ module Cube+) where++import Calculi.Lambda.Cube.Dependent as Cube+import Calculi.Lambda.Cube.HigherOrder as Cube+import Calculi.Lambda.Cube.Polymorphic as Cube+import Calculi.Lambda.Cube.Polymorphic.Unification as Cube+import Calculi.Lambda.Cube.SimpleType as Cube
+ src/Calculi/Lambda/Cube/Dependent.hs view
@@ -0,0 +1,21 @@+module Calculi.Lambda.Cube.Dependent where++import Calculi.Lambda.Cube.SimpleType++{-|+ Typesystems which can have values in their types.+-}+class SimpleType t => Dependent t where+ + {-|+ A value-level term that can be encoded as a type expression.++ Of kind @* -> *@ because it expects a typesystem as a parameter.+ -}+ type DependentTerm t :: * -> *++ {-|+ Encode a value at the type-level. This could be just a constructor or+ a complete transformation of the AST, but this typeclass doesn't care.+ -}+ valueToType :: (DependentTerm t) t -> t
+ src/Calculi/Lambda/Cube/HigherOrder.hs view
@@ -0,0 +1,64 @@+{-# LANGUAGE FlexibleContexts #-}+module Calculi.Lambda.Cube.HigherOrder where++import Calculi.Lambda+import Calculi.Lambda.Cube.SimpleType+import Control.Typecheckable+import qualified Data.Map as Map++{-|+ Typeclass for higher-order types. Classically this would just be checking the+ <https://en.wikipedia.org/wiki/Arity arity> of type constructors but there are+ more complex typesystems that exist that could benefit from allowing an arbitrary+ typechecking ability for a higher-order typesystem.+-}+class (SimpleType t) => HigherOrder t where+ {-|+ The typesystem for the kindedness of type expressions.+ -}+ type Kindsystem t :: *++ {-|+ A typing context for the kindedness of type expressions. Analogue to `TypingContext`.+ -}+ type KindContext t :: *++ {-|+ Type errors for the kindedness of type expressions. Analogue to `TypeError`.+ -}+ type KindError t :: *++ {-|+ Typecheck a type expression.+ -}+ kindcheck :: KindContext t -> t -> Either [KindError t] (KindContext t, Kindsystem t)++ {-|+ More generalised form of `abstract` to work on all type operators, not+ just function types.++ @`typeap` M (∀a. a) = (∀ a. M a)@++ @`typeap` T X = (T X)@++ @`typeap` (`typeap` ((→)) A) B ≡ `abstract` A B@+ -}+ typeap :: t -> t -> t++ {-|+ More generalised form of `reify`, working on all type application.++ @`untypeap` (M x) = Just (M, x)@++ @`untypeap` (X → Y) = Just (((→) X), Y)@++ @`untypeap` X = Nothing@+ -}+ untypeap :: t -> Maybe (t, t)++{-|+ Infix `typeap`.+-}+(/$) :: (HigherOrder t) => t -> t -> t+(/$) = typeap+infixl 8 /$
+ src/Calculi/Lambda/Cube/Polymorphic.hs view
@@ -0,0 +1,299 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE UndecidableInstances #-}+module Calculi.Lambda.Cube.Polymorphic (+ -- * Typeclass for Polymorphic Typesystems+ Polymorphic(..)+ , Substitution(..)+ -- ** Notation and related functions+ , areAlphaEquivalent+ , (≣)+ , (\-/)+ , generalise+ , generalise'+ , polytypesOf+ , boundPolytypesOf+ , monotypesOf+ , isPolyType+ -- ** Typechecking context+ , SubsContext(..)+ , SubsContext'+ -- *** SubsContext lenses+ , subsMade+ , tape+) where++import Calculi.Lambda.Cube.SimpleType+import Data.Either.Combinators+import qualified Data.Map as Map+import qualified Data.Set as Set+import Control.Lens as Lens hiding ((&))++{-|+ A TypingContext+-}+data SubsContext t p = SubsContext {+ _subsMade :: Map.Map p t+ -- ^ The substitutions made so far, where the key is the poly type+ -- that is substituted and the value is what is substituting it.+ , _tape :: [p]+ -- ^ An infinite list of polytypes not present in the who typing context.+} deriving (Eq, Ord)+makeLenses ''SubsContext++{-|+ Datatype describing possible substitutions found by the `substitutions` Polymorphic+ typeclass method.+-}+data Substitution t p =+ Mutual p p+ -- ^ Two equivalent polytypes that could substitute eachother.+ | Substitution t p+ -- ^ A substitution of type expression @t@ over polytype @p@+ deriving (Eq, Ord, Show)++{-|+ Note: only shows the first 10 elements of the infinte list.+-}+instance (Show t, Show p) => Show (SubsContext t p) where+ show (SubsContext s tp) = "SubsContext (" ++ show s ++ ") (" ++ show (take 10 tp) ++ ")"++{-|+ `SubsContext` but assumes the poly type representation of @t@ is the second argument.+-}+type SubsContext' t = SubsContext t (PolyType t)++{-|+ Class of typesystems that exhibit polymorphism.+-}+class (Ord (PolyType t), SimpleType t) => Polymorphic t where++ {-|+ The representation of a poly type, also reffered to as a type variable.+ -}+ type PolyType t :: *++ {-|+ Find the substitutions between two type expressions. If there's+ a mismatch in structure then report the values passed as a Left+ value.++ ===Behaviour++ * A substitution of a poly type \"a\" for mono type \"X\"++ >>> substitutions (X) (a)+ Right [Substitution (X) (a)]++ * Two type expressions have substitutions between eachother.++ >>> substitutions (a → B) (X → b)+ Right [Substitution (X) (a), Substitution (B) (b)]++ * A mutual substitution between two poly types.++ >>> substitutions (a) (b)+ Right [Mutual (a) (b)]++ * Mismatches in structure.++ >>> substitutions (X) (Y)+ Left [(X, Y)]++ >>> substitutions (C → x C) (x C)+ Left [(C → x C, x C)]++ -}+ substitutions :: t -> t -> Either [(t, t)] [Substitution t (PolyType t)]++ {-|+ Substitution application, given one type expression substituting a poly type and a+ target type expression, substitute all instances of the poly type in the target+ type expression with the type expression substituting it.++ ===Behaviour++ * Substituting all instance of \"a\" with \"X\"++ >>> applySubstitution X a (∀ a b. a → b → a)+ (∀ b. X → b → X)@++ * Substitution application in a type expression with a type constructor.++ >>> applySubstitution (X → Y) x (M x)+ (M (X → Y))++ * Applying a substitution to a type expression that doesn't contain the poly type+ being substituted++ >>> applySubstitution Y x (M Q)+ (M Q)+ -}+ applySubstitution :: t -> PolyType t -> t -> t++ {-|+ Quantify instances of a poly type in a type expression.++ ===Behaviour++ * Quantifying a poly type that appears in a type expression.++ >>> quantify a (a → X)+ (∀ a. a → X)++ * Quantifying a poly type that doesn't appear in a type expression++ >>> quantify a (b → X)+ (∀ a. b → X)+ -}+ quantify :: PolyType t -> t -> t++ {-|+ Polymorphic constructor synonym, as many implementations will have a constructor along+ the lines of "Poly p".+ -}+ poly :: PolyType t -> t++ {-|+ Function that retrives all the poly types in a type, quantified+ or not.++ ===Behaviour++ * Type expression with some of it's poly types quantified.++ >>> polytypesOf (∀ a b. a → b → c d))+ Set.fromList [a, b, c, d]++ * Type expression with no quantified poly types.++ >>> polytypesOf (a → b → c)+ Set.fromList [a, b, c]++ * Type expression with no unquantified poly types.++ >>> polytypesOf (∀ c. X → c)+ Set.singleton (c)+ -}+ polytypesOf :: t -> Set.Set t++ {-|+ Function that retrives all the quantified poly types in+ a type expression.++ ===Behaviour++ * Type expression with some of it's poly types quantified.++ >>> quantifiedOf (∀ a b. a → b → c d))+ Set.fromList [a, b]++ * Type expression with no quantified poly types.++ >>> quantifiedOf (a → b → c)+ Set.empty++ * Type expression with no unquantified poly types.++ >>> quantifiedOf (∀ c. X → c)+ Set.singleton (c)+ -}+ quantifiedOf :: t -> Set.Set t++{-|+ Infix `areAlphaEquivalent`+-}+(≣) :: Polymorphic t => t -> t -> Bool+(≣) = areAlphaEquivalent++infix 4 ≣++{-|+ Infix `quantify`, looks a bit like @∀@ but doesn't interfere with unicode syntax extensions.+-}+(\-/) :: Polymorphic t => PolyType t -> t -> t+(\-/) = quantify++infixr 6 \-/++{-|+ All the unbound polytypes in a type expression.+-}+freePolytypesOf :: Polymorphic t => t -> Set.Set t+freePolytypesOf t = polytypesOf t `Set.difference` quantifiedOf t++{-|+ Bound polytypes of an expression.+-}+boundPolytypesOf :: Polymorphic t => t -> Set.Set t+boundPolytypesOf = quantifiedOf++{-|+ Monotypes of a type expression.+-}+monotypesOf :: Polymorphic t => t -> Set.Set t+monotypesOf t = Set.difference (bases t) (polytypesOf t)++{-|+ Quantify every free polytype in a type expression, excluding a+ set of polytypes to not quantify.++ >>> generalise Set.empty (x → y)+ (∀ x y. x → y)++ >>> generalise (Set.fromList [a, b]) (a → b → c)+ (∀ c. a → b → c)+-}+generalise :: forall t. Polymorphic t => Set.Set t -> t -> t+generalise exclude t = foldr quantify t ftvsBare where+ ftvsBare :: Set.Set (PolyType t)+ ftvsBare = Set.fromList $ snd <$> filter (flip Set.member ftvs . fst) polyTypes where+ ftvs = Set.difference (freePolytypesOf t) exclude+ polyTypes :: [(t, PolyType t)]+ polyTypes = fmap (\(Mutual a b) -> (poly a, b)) . fromRight [] $ substitutions t t++{-|+ `generalise` but with an empty exclusion set.+-}+generalise' :: Polymorphic t => t -> t+generalise' = generalise Set.empty++{-|+ Check if two types are equivalent, where equivalence is defined as the substitutions+ being made being symbolically identical, where binds and poly types appear in+ the same place but may have different names (this is Alpha Equivalence).++ >>> areAlphaEquivalent (∀ a. X → a) (∀ z. X → z)+ True++ >>> areAlphaEquivalent (M → X) (M → X)+ True++ >>> areAlphaEquivalent (∀ a. a) (∀ z. z → z)+ False+-}+areAlphaEquivalent :: forall t. Polymorphic t => t -> t -> Bool+areAlphaEquivalent x y = fromRight False $ all isMutual <$> subs where+ subs = substitutions x y++ isMutual (Mutual _ _) = True+ isMutual _ = False++{-|+ Tests if a type expression is a base poly type.++ >>> isPolyType (∀ a. a)+ False++ >>> isPolyType (a)+ True++ >>> isPolyType (b → c)+ False+-}+isPolyType :: Polymorphic t => t -> Bool+isPolyType t =+ fromRight False $ substitutions t t <&> \case+ [Mutual a b] -> a == b && t == poly a+ _ -> False
+ src/Calculi/Lambda/Cube/Polymorphic/Unification.hs view
@@ -0,0 +1,422 @@+{-|+ Module containing functions related to solving and unifying+ polymorphic type expressions.+-}+module Calculi.Lambda.Cube.Polymorphic.Unification (+ -- * Unification related functions+ unify+ , unifyGr+ , (⊑)+ , (\<)+ , hasSubstitutions+ , applyAllSubs+ , applyAllSubsGr+ , unvalidatedApplyAllSubs+ , resolveMutuals+ -- * Substitution validation+ -- ** Substitution error datatypes+ , SubsErr(..)+ , ConflictTree+ -- ** Validation and analysis functions+ , substitutionGraph+ , substitutionGraphGr+ , substitutionGraphM+ , topsortSubs+ , topsortSubsG+ , occursCheck+ , conflicts+) where++import Calculi.Lambda.Cube.Polymorphic+import Control.Lens as Lens+import Control.Monad+import Control.Monad.State+import Data.Bifunctor+import Data.Either.Combinators+import Data.Either (partitionEithers)+import Data.Graph.Inductive as Graph hiding ((&))+import Data.Graph.Inductive.Helper+import Data.List.Ordered+import Data.List (group)+import Data.Maybe+import qualified Data.Set as Set+import Data.Tree++{-+ MODULE TODO:+ We need a way to differeciate between two instances of the same type expression, otherwise+ unifying two instances of the same type expression will frequently return cyclic substitution+ errors.++ Alternatively, this is fretting over nothing or is something writers of code using this library+ should do themselves.+-}++{-|+ Errors in poly type substitution.+-}+data SubsErr gr t p =+ MultipleSubstitutions (ConflictTree t p)+ -- ^ A `ConflictTree` of substitutions leading to `p`+ | CyclicSubstitution (gr t p)+ -- ^ There is a cycle of substitutions.+ | SubsMismatch t t+ -- ^ A substitution between two incompatable type expressions+ -- was attempted. (i.e. @`substitutions` (X) (Y → Y)@)+ deriving (Eq, Show, Read)++{-|+ A substitution conflict's root, with a tree of types substituting+ variables as the first element [1] and the second element being the+ type where these clashing substitutions converge.++ [1]: to be read that the first element of the tuple is a forest of+ substitutions leading the final type expression with a substitution conflict.++ TODO: Put a diagram here instead.+-}+type ConflictTree t p = ([Tree (t, [p])], t)++{-|+ `substitutions` but takes place in an Either that catches substitution errors.+-}+substitutionsM :: (Polymorphic t, p ~ PolyType t) => t -> t -> Either [SubsErr gr t p] [Substitution t p]+substitutionsM t1 t2 = fmap (uncurry SubsMismatch) `first` substitutions t1 t2++{-|+ This module's namesake function.++ <https://en.wikipedia.org/wiki/Unification_(computer_science) Unification>+ is an important step of typechecking polymorphic lambda calculi, taking two+ type expressions and computing their differences to produce a sequence+ of substitutions needed to make both type expressions equivalent.++ This implementation computes a list of substitutions with the substitutions+ to be applied first at the end of the list and the ones to be applied+ last at the beginning. This is an artifact of how the reordering of the substitutions+ works and can be remedied with a `reverse` if needed.++ ===Behaviour+ * Unifying two compatable type expressions++ >>> unify (forall a. a) (A → B)+ Right [(A → B, a)]++ >>> unify (forall a b c. a → (b → c) → a) (forall x. x → (I → x) → G)+ Right [(G, a), (G, c), (G, x), (I, b)]++ * Unifying incompatable type expressions yeilds errors.++ >>> unify (A) (B)+ Left [SubsMismatch A B]++ * Unifying a poly type with a type expression that contains that poly type yeilds a+ cyclic substitution error.++ >>> unify (a) (F a)+ Left [CyclicSubstitution (mkGraph [(2,(F a))] [(2,2,(a))])]]+ -- The above is a graph showing the cycle of (F a) trying to substitute it's own poly type (a)++ * Unifying equivalent type expressions yeilds empty lists.++ >>> unify (forall a. a → C) (forall x. x → C)+ Right []++ >>> unify (X → Y) (X → Y)+ Right []+-}+unify :: forall gr t p. (Polymorphic t, p ~ PolyType t, DynGraph gr)+ => t -- ^ The first type expression+ -> t -- ^ The second type expression+ -> Either [SubsErr gr t p] [(t, p)] -- ^ The result from trying to unify both type expressions.+unify t1 t2 = do+ -- Find the substitutions and partition them into mutuals and substitutions+ subs <- resolveMutuals <$> substitutionsM t1 t2+ -- validate and order the substitutions+ topsortSubsG <$> substitutionGraph subs++{-|+ `unify` with `Gr` as the instance for DynGraph.+-}+unifyGr :: forall t p. (Polymorphic t, p ~ PolyType t)+ => t+ -> t+ -> Either [SubsErr Gr t p] [(t, p)]+unifyGr = unify++{-|+ Partition a list of `Substitution`s into it's mutuals (first element of the tuple) and+ it's substitutions (second element).+-}+partitionSubstitutions :: [Substitution t p] -> ([(p, p)], [(t, p)])+partitionSubstitutions =+ partitionEithers . fmap (\case (Mutual x y) -> Left (x, y); (Substitution x y) -> Right (x, y);)++{-|+ Test to see if two types have valid substitutions between eachother.+-}+hasSubstitutions :: forall t p. (Polymorphic t, p ~ PolyType t) => t -> t -> Bool+hasSubstitutions t1 t2 = isRight (unify t1 t2 :: Either [SubsErr Gr t p] [(t, p)])++{-|+ Given a list of substitutions, resolve all the mutual substitutions and+ return a list of substitutions in the form @(t, p)@.+-}+resolveMutuals :: forall t p. (Polymorphic t, p ~ PolyType t)+ => [Substitution t p] -- ^ The list of mixed (see `Substitution`) substitutions.+ -> [(t, p)] -- ^ The resulting list of substitutions+resolveMutuals subs =+ let (mutuals, subs') = partitionSubstitutions subs+ -- As a mutual substitution (a,b) means that a is b, every substitution+ -- of the form (T, a) must be duplicated to include (T, b), and every+ -- substitution of the form (M, b) must be duplicated to include (M, a).++ -- If a future maintainer changes this to a foldl, they should reverse the+ -- output of sortMutuals (if that's stil a part of this code).+ in foldr expandMutual subs' (sortMutuals subs' mutuals) where+ expandMutual :: (p, p) -> [(t, p)] -> [(t, p)]+ expandMutual (a, b) _subs = do+ -- Get the single substitution+ sub@(term, var) <- _subs+ -- if either a or b are equal to var then duplicate the substitution.+ if a == var || b == var then [(term, a), (term, b)] else return sub++ {-+ Reorder the mutuals so that they're resolved in an order that+ doesn't miss out on duplications.++ NOTE: This is a bodge, a proper topsort of these needs to be done as part+ of a graph transform, probably.+ NOTE: re: above. Extensive tests haven't really come up with a contradiction+ to this working, so maybe it's okay? I don't trust it though.+ -}+ sortMutuals :: [(t, p)] -> [(p, p)] -> [(p, p)]+ sortMutuals _subs = sortOn (\(a, b) -> max (subCount a) (subCount b)) where+ -- Find the number of times a polytype is substituted (Should be 1 or 0, could be more+ -- but that'll be caught by the occurs check later).+ subCount :: p -> Integer+ subCount sub = foldr (\(_, sub') -> if sub' == sub then (+ 1) else id ) 0 _subs++{-|+ Type ordering operator, true if the second argument is more specific or equal to+ the first.++ ===Behaviour++ * A type expression with poly types being ordered against one without them.++ >>> (∀ a. a) ⊑ (X → Y)+ True++ * A type expression being ordered against itself, displaying reflexivity.++ >>> (X → X) ⊑ (X → X)+ True++ * All type expressions are more specific than a type expression+ of just a single (bound or unbound) poly type.++ >>> (a) ⊑ (a)+ True++ >>> (a) ⊑ (b)+ True++ >>> (a) ⊑ (X)+ True++ >>> (a) ⊑ (X → Y)+ True++ etc.+-}+(⊑) :: (Polymorphic t) => t -> t -> Bool+t ⊑ t' = fromRight False $ do+ subs <- resolveMutuals <$> substitutionsM t' t+ applySubs <- applyAllSubsGr subs+ return (t' ≣ applySubs t)++infix 4 ⊑++{-|+ Non-unicode @⊑@.+-}+(\<) :: (Polymorphic t) => t -> t -> Bool+(\<) = (⊑)++infix 4 \<++{-|+ For a given list of substitutions, either find and report inconsistencies+ through `SubsErr` or compute a topsort by order of substitution such that for+ a list of substitutions @[a, b, c]@ c should be applied, then b, then a.++ This backward application is a product of how the graph used to compute+ the reordering is notated and how topsorting is ordered. In this+ graph for nodes @N, M@ and egde label @p@, @N --p-> M@ notates that+ all instances of @p@ in @M@ will be substituted by @N@. In regular topsort+ this means that @N@ will preceed @M@ in the list, but this doesn't make sense+ when we topsort to tuples of the form @(N, p)@.+-}+topsortSubs :: forall gr t p. (DynGraph gr, Polymorphic t, p ~ PolyType t)+ => [(t, p)]+ -> Either [SubsErr gr t p] [(t, p)]+topsortSubs = fmap topsortSubsG . (substitutionGraph :: [(t, p)] -> Either [SubsErr gr t p] (gr t p))++{-|+ A version of `topsortSubs` that takes an already generated graph rather than+ building it's own.++ If given a graph with cycles or nodes with 2 or more inward edges of the same label+ then there's no garuntee that the substitutions will be applied correctly.+-}+topsortSubsG :: forall gr t p. (Graph gr)+ => gr t p+ -> [(t, p)]+topsortSubsG = unvalidatedEdgeyTopsort++{-|+ Without validating if the substitutions are consistent, fold them into a single+ function that applies all substitutions to a given type expression.+-}+unvalidatedApplyAllSubs :: (Polymorphic t, p ~ PolyType t)+ => [(t, p)]+ -> t+ -> t+unvalidatedApplyAllSubs = foldr (\sub f -> uncurry applySubstitution sub . f) id++{-|+ Validate substitutions and fold them into a single substitution function.+-}+applyAllSubs :: forall gr t p. (Polymorphic t, p ~ PolyType t, DynGraph gr)+ => [(t, p)]+ -> Either [SubsErr gr t p] (t -> t)+applyAllSubs = fmap unvalidatedApplyAllSubs . topsortSubs++{-|+ `applyAllSubs` using fgl's `Gr`.+-}+applyAllSubsGr :: (Polymorphic t, p ~ PolyType t)+ => [(t, p)]+ -> Either [SubsErr Gr t p] (t -> t)+applyAllSubsGr = applyAllSubs++{-|+ Function that builds a graph representing valid substitutions or reports+ any part of the graph's structure that would make the substitutions invalid.+-}+substitutionGraph+ :: forall gr t p. (Polymorphic t, p ~ PolyType t, DynGraph gr)+ => [(t, p)]+ -> Either [SubsErr gr t p] (gr t p)+substitutionGraph subs =+ let (errs, (_, graph :: gr t p)) = run empty (substitutionGraphM subs)+ in if null errs then Right graph else Left errs++{-|+ `substitutionGraph` using fgl's `Gr`.+-}+substitutionGraphGr :: forall t p. (Polymorphic t, p ~ PolyType t)+ => [(t,p)]+ -> Either [SubsErr Gr t p] (Gr t p)+substitutionGraphGr = substitutionGraph++{-|+ A version of `substitutionGraph` that works within fgl's NodeMap state monad.+-}+substitutionGraphM+ :: forall t p gr. -- No haddock documentation for constraints, but putting this here anyway+ ( Polymorphic t -- The typesystem @t@ is a an instance of Polymorphic+ , p ~ PolyType t -- @p@ is @t@'s representation of poly types+ , Ord p -- t's representation of poly types is ordered+ , DynGraph gr -- the graph representation is an instance of DynGraph+ )+ => [(t, p)] -- ^ A list of substitutions+ -> NodeMapM t p gr [SubsErr gr t p]+ -- ^ A nodemap monadic action where the graph's edges are substitutions+ -- and the nodes are type expressions.+substitutionGraphM subs = do+ {-+ Construct the graph so we have something to work with.+ -}+ -- Assemble a list of all the type expressions, including the substitution targets+ {- Note: to make this work from a point of theory, all the targets in "subs" are turned into+ type expressions using the polymorphic constructor, allowing all substitutions to+ have at least one edge from the substitutions to the targets. -}+ let typeExprs = nubSort $ subs >>= (\(t, p) -> [t, poly p])+ -- Build a list of type expressions and their poly types.+ let basesList = (\t -> (t, polytypesOf t)) <$> typeExprs+ -- Why not freeTypeVariables?+ -- Because during random tests the case where a variable was+ -- quantified in different areas happened a bunch.+ -- Construct the edges+ let subsEdges = buildEdge <$> subs <*> basesList+ -- Insert the nodes. (crashes if this isn't done first, because fgl!)+ void (insMapNodesM typeExprs)+ -- Insert the edges.+ insMapEdgesM (catMaybes subsEdges)+ -- Compute and return the errors+ gets (occursCheck . snd) where+ {-+ Given a substitution pair and pair of a type expression and it's+ base types, check if the substitution's own target appears in those+ base types.+ -}+ buildEdge :: (t, p) -> (t, Set.Set t) -> Maybe (t, t, p)+ buildEdge (t1, p) (t2, t2'bases)+ | poly p `Set.member` t2'bases = Just (t1, t2, p)+ | otherwise = Nothing++{-|+ From a graph representing substitutions of variables @p@ in terms @t@, where+ edges represent the origin node replacing the variable represented by the edge label+ in the target node.++ e.g. The edge @(N, (x -> x), x)@ corresponds to replacing all instances of the variable @x@ in+ @(x -> x)@ with @N@.+-}+occursCheck :: forall gr t p. (DynGraph gr, Ord p, Ord t) => gr t p -> [SubsErr gr t p]+occursCheck graph =+ let cycles = cyclicSubgraphs graph+ clashes = clashesOfGraph graph+ in if not (null cycles) then+ -- If ther are cycles, return them after passing them through the error constructor.+ CyclicSubstitution <$> cycles+ else if not (null clashes) then+ MultipleSubstitutions <$> clashes+ else [] where+ {-+ Generate a list of trees of fully labelled edges,+ -}+ clashesOfGraph :: gr t p -> [ConflictTree t p]+ clashesOfGraph graph =+ uncurry (branchConflicts graph) <$> conflicts graph++{-|+ Find all contexts with non-unique inward labels, paired with each+ label that wasn't unique.+-}+conflicts :: (DynGraph gr, Ord p, Ord t) => gr t p -> [(p, Graph.Context t p)]+conflicts graph = do+ -- For each node in the graph...+ node <- nodes graph+ --Find it's inward edges and group them by label, filtering any label that appears once.+ conflict <- nub =<< filter hasSome (group (inn graph node <&> (^._3)))+ return (conflict, context graph node)++{-|+ Given a graph, a conflicting label, and the node where the label is conflicting;+ branch out towards it's roots.+-}+branchConflicts :: (DynGraph gr, Ord p, Ord t) => gr t p -> p -> Graph.Context t p -> ([Tree (t, [p])], t)+branchConflicts graph lbl ctx@(_,nn,nl,_) = flip (,) nl $ do+ -- Get all the inward edges+ let inward = filter ((== lbl) . (^._3)) (inn graph nn)+ -- Reverse depth-first search to find all the roots, using the contexts+ -- as the tree's value.+ tree <- rdffWith id ((^._1) <$> inward) graph+ -- process the tree,+ return $ processTree ctx tree where+ processTree :: Graph.Context t p -> Tree (Graph.Context t p) -> Tree (t, [p])+ processTree pctx (Node ctx forest) =+ Node (lab' ctx, fst <$> filter ((== node' pctx) . snd) (ctx^._4)) (processTree ctx <$> forest)
+ src/Calculi/Lambda/Cube/SimpleType.hs view
@@ -0,0 +1,200 @@+{-|+ Module describing a typeclass for types with stronger mathematical foundations that+ represents a type system for simply-typed lambda calculus (λ→ on the lambda cube).+-}+module Calculi.Lambda.Cube.SimpleType (+ -- * Typeclass for λ→+ SimpleType(..)+ -- ** Notation and related functions+ , (====)+ , (/->)+ , order+ -- * Typechecking+ , SimpleTypingContext(..)+ , SimpleTypeErr(..)+ , variables+ , constants+ , allTypes+ -- * Other functions+ , prettyprintST+ , isFunction+ , isBase+ , basesOfExpr+ , envFromExpr+) where++import Calculi.Lambda+import Control.Monad+import Control.Lens+import Data.Bifoldable+import Data.List+import qualified Data.Map as Map+import Data.Maybe+import Data.Monoid+import qualified Data.Set as Set+import Test.QuickCheck++{-|+ A simple typing context.+-}+data SimpleTypingContext c v t = SimpleTypingContext {+ _variables :: Map.Map v t+ -- ^ A mapping of variables to types.+ , _constants :: Map.Map c t+ -- ^ A mapping of constants to types.+ , _allTypes :: Set.Set t+ -- ^ All the base types in scope.+} deriving (Show, Read, Eq, Ord)++{-|+ Type errors that can occur in a simply-typed lambda calculus.+-}+data SimpleTypeErr t =+ NotAFunction t+ -- ^ Attempted to split a type (a -> b) into (Just (a, b)), but the type wasn't+ -- a function type.+ | UnexpectedType t t+ -- ^ The first type was expected during typechecking, but the second type was found.+ deriving (Eq, Ord, Show)++makeLenses ''SimpleTypingContext++{-|+ Typeclass based off simply-typed lambda calculus + a method for getting all+ the base types in a type.+-}+class (Ord t) => SimpleType t where+ {-|+ The representation of a Mono type, also sometimes referred to a type constant.++ in the type expression @A → M@, both @A@ and @M@ are mono types, but in a polymorphic+ type expression such as @∀ a. a → X@, @a@ is not a mono type.+ -}+ type MonoType t :: *++ {-|+ Given two types, generate a new type representing the type of a function from+ the first type to the second.++ @`abstract` K D = (K → D)@++ When polymorphism is present:++ @`abstract` (∀ a. a) T = (∀ a. a → T)@++ @`abstract` a t = (a → t)@+ -}+ abstract :: t -> t -> t++ {-|+ Given a function type, decompose it into it's argument and return types. Effectively+ the inverse of `abstract` but returns `Nothing` when the type isn't a function type.++ @`reify` (K → D) = Just (K, D) @++ @`reify` (K) = Nothing@++ When polymorphism is present:++ @`reify` (∀ a. a → T) = Just (∀ a. a, t)@++ @`reify` (a → T) = Just (a, t)@++ `reify` is almost the inverse of `abstract`, and the following property should hold true:++ prop> fmap (uncurry abstract) (reify t) = Just t++ -}+ reify :: t -> Maybe (t, t)++ {-|+ Given a type, return a set of all the base types that occur within the type.++ @`bases` (∀ a. a) = Set.singleton (a)@++ @`bases` (M X → (X → Z) → M Z) = Set.fromList [M, X, Z] -- or Set.fromList [M, X, Z, →], depending@+ -}+ bases :: t -> Set.Set t++ {-|+ Polymorphic constructor synonym, as many implementations will have a constructor along+ the lines of "Mono m".+ -}+ mono :: MonoType t -> t++ {-|+ Type equivalence, for simple typesystems this might be `(==)` but for polymorphic or+ dependent typesystems this might also include alpha equivalence or reducing the+ type expressions to normal form before performing another equivalence check.+ -}+ equivalent :: t -> t -> Bool++{-|+ Infix `equivalent`.+-}+(====) :: SimpleType t => t -> t -> Bool+(====) = equivalent++infix 4 ====++{-|+ Infix `abstract` with the appearence of @↦@, which is used to denote function+ types in much of mathematics.+-}+(/->) :: SimpleType t => t -> t -> t+(/->) = abstract++infixr 7 /->++{-|+ Find the depth of a type.++ @`order` (M → X) = 1@++ @`order` ((M → Y) → X) = 2@++ @`order` (M → ((Y → Q) → Z) → X) = 2@++ @`order` X = 0@+-}+order :: SimpleType t => t -> Integer+order t = case reify t of+ Nothing -> 0+ Just (t1, t2) -> max (1 + order t1) (order t2)++{-|+ given a function that prettyprints base types, pretty print the type with function arrows+ whenever a function type is present.+-}+prettyprintST :: SimpleType t => (t -> String) -> t -> String+prettyprintST f t =+ case reify t of+ Nothing -> f t+ Just (t1, t2) ->+ let t1'str = if isFunction t1 then "(" ++ prettyprintST f t1 ++ ")" else prettyprintST f t1+ in t1'str ++ " -> " ++ prettyprintST f t2++{-|+ Check if a simple type is a function type.+-}+isFunction :: SimpleType t => t -> Bool+isFunction = isJust . reify++{-|+ Check if a simple type is a base type.+-}+isBase :: SimpleType t => t -> Bool+isBase = not . isFunction++{-|+ Function retrives a set of all base types in the given lambda expression.+-}+basesOfExpr :: SimpleType t => LambdaTerm c v t -> Set.Set t+basesOfExpr = bifoldr (\_ st -> st) (\t st -> bases t <> st) Set.empty++{-|+ Get a typing environment that assumes all the base types in an expression+ are valid.+-}+envFromExpr :: SimpleType t => LambdaTerm c v t -> SimpleTypingContext c v t+envFromExpr = SimpleTypingContext Map.empty Map.empty . basesOfExpr
+ src/Calculi/Lambda/Cube/TH.hs view
@@ -0,0 +1,169 @@+module Calculi.Lambda.Cube.TH (+ -- sfo+ sf+ , stlc+) where++import qualified Language.Haskell.TH as TH+import qualified Language.Haskell.TH.Quote as TH+import qualified Language.Haskell.TH.Syntax as TH+import qualified Compiler.Typesystem.SystemFOmega as SFO+import qualified Compiler.Typesystem.SystemF as SF+import qualified Compiler.Typesystem.SimplyTyped as STLC+import Text.Megaparsec+import Calculi.Lambda.Cube+import Data.List+import Control.Monad++-- | Lambda Cube parsec type.+type LCParsec = Parsec String+-- | SystemFOmega with mono and poly types represented as strings.+-- type StringSFO = SFO.SystemFOmega String String (Maybe (STLC.SimplyTyped String))+-- | SystemF with mono and poly types represented as strings.+type StringSF = SF.SystemF String String+-- | SimplyTyped with mono types represented as strings.+type StringSTLC = STLC.SimplyTyped String++{-|+ Lambda Cube symbol wrapper for strings.+-}+lamcsymbol :: String -> LCParsec String+lamcsymbol = lamctoken . string++{-|+ Lambda Cube parser token wrapper, expects the token followed by 0 or more spaces.+-}+lamctoken :: LCParsec a -> LCParsec a+lamctoken p = do+ pval <- p+ void $ many (char ' ')+ return pval++{-|+ Parenthesis parser combinator.+-}+paren :: LCParsec a -> LCParsec a+paren = between (lamcsymbol "(") (lamcsymbol ")")++{-|+ Wrapper that allows preceeding whitespace before a token and then expects the+ input to end.+-}+wrapped :: LCParsec a -> LCParsec a+wrapped p = do+ void $ many (lamcsymbol " ")+ p' <- p+ eof+ return p'++{-|+ Parser for a bare variable, notated by beginning with a lowercase character.+-}+variable :: LCParsec String+variable = lamctoken ((:) <$> lowerChar <*> many (lowerChar <|> upperChar)) <?> "variable"++{-|+ Parser for a bare constant, notated by beginning with an uppercase character.+-}+constant :: LCParsec String+constant = lamctoken ((:) <$> upperChar <*> many (lowerChar <|> upperChar)) <?> "constant"++{-|+ Given a type expression parser for a Polymorphic typesystem, parse a forall+ quantification (@∀ a b c. <expr>@ or @forall a b c. <expr>@) followed by+ the expression parser that was passed to it.+-}+quant :: (Polymorphic t, String ~ PolyType t) => LCParsec t -> LCParsec t+quant pexpr = label "quantification" $ do+ -- Parse the prefix for quantification+ void $ lamcsymbol "∀" <|> lamcsymbol "forall"+ -- Parse one or more variables+ tvars <- some variable+ -- terminate the quantification expression with a period+ void $ lamcsymbol "."+ -- parse the expression with the parser passed to this function+ expr <- pexpr+ -- quantify each variable over the expression that was passed.+ return (foldr quantify expr tvars)++{-|+ given a subexpression parser, parse a sequence of subexpressions+ seperated by function arrows.+-}+exprsequence :: SimpleType t => LCParsec t -> LCParsec t+exprsequence subexpr = label "expression sequence" $ do+ -- parse as many subexpressions as we can (at least 1 though)+ expr <- subexpr+ -- optionally parse a function tail if it is present+ funApply <- optional $ do+ void $ lamcsymbol "->" <|> lamcsymbol "→"+ exprsequence subexpr+ -- if after the initial sequence it turned out this was the first+ -- argument to a function expression, then we apply it as the first argument.+ return (maybe expr (expr /->) funApply)+{-+sfoexpr :: LCParsec StringSFO+sfoexpr = label "System-Fω expression" $+ quant sfoexpr+ <|> exprsequence (fmap (foldl1 (/$)) <$> some $+ poly <$> variable+ <|> mono <$> constant+ <|> paren sfoexpr)+-}+sfexpr :: LCParsec StringSF+sfexpr = label "System-F expression" $+ quant sfexpr+ <|> exprsequence (poly <$> variable+ <|> mono <$> constant+ <|> paren sfexpr)++stlcexpr :: LCParsec StringSTLC+stlcexpr = label "Simply-typed expression" $ exprsequence (mono <$> constant <|> paren stlcexpr)++{-+{-|+ A QuasiQuoter for SystemFOmega, allowing arbitrary type application++ @[sfo| forall x. R x -> M x |] == quantify \"x\" (mono \"R\" /$ poly \"x\" /-> mono \"M\" /$ poly \"x\")@+-}+sfo :: TH.QuasiQuoter+sfo = mkqq "sfo" sfoexpr+-}+{-|+ A QuasiQuoter for SystemF, allowing quantification and poly types (lower case).++ @[sf| forall a b. a -> b |] == quantify \"a\" (quantify \"b\" (poly \"a\" \/-> poly \"b\"))@++-}+sf :: TH.QuasiQuoter+sf = mkqq "sf" sfexpr++{-|+ A QuasiQuoter for SimplyTyped.++ @[stlc| A -> B -> C |] == mono \"A\" \/-> mono \"B\" \/-> mono \"C\"@++ @[stlc| (A -> B) -> B |] == (mono \"A\" \/-> mono \"B\") \/-> mono \"B\"@+-}+stlc :: TH.QuasiQuoter+stlc = mkqq "stlc" stlcexpr++{-|+ Helper to generate a QuasiQuoter for an arbitrary parser with a liftable type.+-}+mkqq :: TH.Lift t => String -> LCParsec t -> TH.QuasiQuoter+mkqq pname p = TH.QuasiQuoter {+ TH.quoteExp = \str -> do+ loc <- TH.location+ let fname = intercalate ":" [pname+ , TH.loc_filename loc+ , show $ TH.loc_start loc+ , show $ TH.loc_end loc+ ]+ case runParser (wrapped p) fname str of+ Left err -> fail . show $ err+ Right val -> TH.lift val+ , TH.quotePat = error $ pname ++ " doesn't implement quotePat for this QuasiQuoter"+ , TH.quoteType = error $ pname ++ " doesn't implement quoteType for this QuasiQuoter"+ , TH.quoteDec = error $ pname ++ " doesn't implement quoteDec for this QuasiQuoter"+}
+ src/Compiler/Typesystem/Hask.hs view
@@ -0,0 +1,52 @@+{-|+ Re-export of the type expression AST exposed by TemplateHaskell with instances+ of `SimpleType`, `HigherOrder`, and `Polymorphic`.+-}+module Compiler.Typesystem.Hask (+ Type(..)+ , Name(..)+) where++import Language.Haskell.TH.Syntax as TH (Type(..), Name(..), TyVarBndr(..))+import Calculi.Lambda.Cube.HigherOrder+import Calculi.Lambda.Cube.Polymorphic+import Calculi.Lambda.Cube.SimpleType+import Control.Typecheckable+import qualified Data.Set as Set+import Data.Semigroup++instance SimpleType Type where++ type MonoType Type = Name++ abstract a b = (ArrowT `AppT` a) `AppT` b++ reify ((ArrowT `AppT` a) `AppT` b) = Just (a, b)+ reify _ = Nothing++ mono = ConT++ bases = \case+ ForallT binds _ texpr -> bases texpr+ AppT arg ret -> bases arg <> bases ret+ SigT texpr _ -> bases texpr+ a -> Set.singleton a++ equivalent = areAlphaEquivalent++instance Polymorphic Type where++ type PolyType Type = Name++ substitutions = curry $ \case+ (ForallT _ _ texpr1, texpr2) -> substitutions texpr1 texpr2+ (texpr1 , ForallT _ _ texpr2) -> substitutions texpr1 texpr2+ (SigT texpr1 _ , texpr2) -> substitutions texpr1 texpr2+ (texpr1 , SigT texpr2 _) -> substitutions texpr1 texpr2+ (VarT v1 , VarT v2) -> Right [Mutual v1 v2]+ (VarT v , texpr) -> Right [Substitution texpr v]+ (texpr , VarT v) -> Right [Substitution texpr v]+ (AppT arg1 ret1 , AppT arg2 ret2) -> substitutions arg1 arg2 <><> substitutions ret1 ret2+ (texpr1 , texpr2)+ | texpr1 == texpr2 -> Right []+ | otherwise -> Left [(texpr1, texpr2)]
+ src/Compiler/Typesystem/SimplyTyped.hs view
@@ -0,0 +1,131 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE UndecidableInstances #-}+module Compiler.Typesystem.SimplyTyped where++import Calculi.Lambda+import Calculi.Lambda.Cube.SimpleType+import Control.Typecheckable+import Control.Monad+import qualified Control.Monad.State as State+import Data.Bifunctor+import Data.Generics+import qualified Data.Map as Map+import Data.Random.Generics+import Data.Semigroup+import qualified Data.Set as Set+import Test.QuickCheck+import qualified Language.Haskell.TH.Lift as TH++{-|+ Data type describing a type system for simply-typed lambda calculus (λ→).+-}+data SimplyTyped m =+ Mono m+ | Function (SimplyTyped m) (SimplyTyped m)+ deriving (Show, Read, Eq, Ord, Data)++TH.deriveLift ''SimplyTyped++instance Functor SimplyTyped where+ fmap f = \case+ Mono m -> Mono (f m)+ Function from to -> Function (fmap f from) (fmap f to)++instance Foldable SimplyTyped where+ foldr f z = \case+ Mono m -> f m z+ Function from to -> foldr f (foldr f z to) from++instance Ord m => SimpleType (SimplyTyped m) where+ type MonoType (SimplyTyped m) = m++ abstract = Function++ reify (Function from to) = Just (from, to)+ reify _ = Nothing++ bases (Mono m) = Set.singleton (Mono m)+ bases (Function from to) = bases from `Set.union` bases to++ mono = Mono++ equivalent = (==)++data SimplyTypedErr c v t =+ STNotKnownErr (NotKnownErr c v t)+ | STSimpleTypeErr (SimpleTypeErr t)+ deriving (Eq, Ord, Show)++instance (Ord m, Ord c, Ord v) => Typecheckable (LambdaTerm c v) (SimplyTyped m) where+ type TypingContext (LambdaTerm c v) (SimplyTyped m) = (SimpleTypingContext c v (SimplyTyped m))++ type TypeError (LambdaTerm c v) (SimplyTyped m) =+ -- Using an ErrorContext because it can hold a lot of information.+ ErrorContext'+ (LambdaTerm c v)+ (SimplyTyped m) (SimplyTypedErr c v (SimplyTyped m))++ typecheck env _expr =+ -- Always add the current expression to all the errors that have occurred+ -- so there's a list of expressions towards the error that happened.+ first (fmap (\err -> err { _expression = _expr : _expression err }))+ $ case _expr of+ {-+ Case of a LC variable, not really typechecking but instead+ checking that the variable name is in scope.+ -}+ Variable v ->+ let -- If there's an error on the var lookup, return this as the error.+ err = Left [ErrorContext [] env (STNotKnownErr (UnknownVariable v))]+ -- If it succeeds in it's lookup, pipe the result into a tuple in a Right value.+ success = (Right . (,) env)+ in maybe err success (Map.lookup v (_variables env))++ {-+ Application of two expressions.+ -}+ (Apply fun arg) ->+ let -- Typecheck both the function side and the argument+ fun' = typecheck env fun+ arg' = typecheck env arg+ in case (fun', arg') of+ -- If both errored, then combine the errors.+ (Left fun'err, Left arg'err) -> Left $ fun'err <> arg'err+ _ -> do+ -- discard their contexts+ (_, fun'type) <- fun'+ (_, arg'type) <- arg'+ case reify fun'type of+ Nothing ->+ -- The first expression's type wasn't a function type.+ Left [ErrorContext [fun] env (STSimpleTypeErr $ NotAFunction fun'type)]+ Just (funarg'type, funret'type)+ | funarg'type /= arg'type ->+ -- The type of the argument expression doesn't match the expected+ -- type of the function expression.+ Left [ErrorContext [fun] env (STSimpleTypeErr $ UnexpectedType funarg'type arg'type)]+ | otherwise ->+ -- succeeded in typechecking.+ Right (env, funret'type)++ {-+ Abstracting a variable over an expression.+ -}+ (Lambda (var, var'type) expr) -> do+ -- Get any types in var'type not in the set of all types+ -- as every type should be declared by the environment+ -- before appearing in an expression.+ let unknownTypes = Set.toList $ Set.difference (bases var'type) (_allTypes env)+ let errFun t = ErrorContext [] env (STNotKnownErr$ UnknownType t)+ -- If there are unknown types, error on them.+ unless (null unknownTypes) . Left $ errFun <$> unknownTypes+ -- If we get ths far, then var'type was valid+ -- Set a new typing context with var brought into scope+ let env' = env { _variables = Map.insert var var'type (_variables env) }+ -- Typecheck the lambda's body+ (_, expr'type) <- typecheck env' expr+ -- Return the environment and the type of the lambda expression.+ return (env, var'type /-> expr'type)++instance (Data m, Arbitrary m) => Arbitrary (SimplyTyped m) where+ arbitrary = sized $ generatorPWith [alias (\() -> arbitrary :: Gen m)]
+ src/Compiler/Typesystem/SystemF.hs view
@@ -0,0 +1,248 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE StandaloneDeriving #-}+module Compiler.Typesystem.SystemF where++import Data.Bifunctor.TH+import Calculi.Lambda+import Calculi.Lambda.Cube.SimpleType+import Calculi.Lambda.Cube.Polymorphic+import Calculi.Lambda.Cube.Polymorphic.Unification+import Control.Typecheckable+import Control.Monad+import Control.Monad.State+import Control.Monad.Except+import Control.Lens hiding (elements)+import Data.Either.Combinators+import qualified Data.Set as Set+import qualified Data.Map as Map+import Data.Traversable+import Data.List+import Data.Random.Generics+import Data.Generics+import Data.Semigroup+import Data.Maybe+import Data.Graph.Inductive (Gr)+import Test.QuickCheck+import qualified Language.Haskell.TH.Lift as TH++{-|+ An implementation of System-F, similar to haskell's own typesystems but without+ type-level functions beyond (→)+-}+data SystemF m p =+ Mono m+ | Poly p+ | Function (SystemF m p) (SystemF m p)+ | Forall p (SystemF m p)+ deriving (Eq, Ord, Data)++instance (Ord m, Ord p, Show m, Show p) => Show (SystemF m p) where+ show (Mono m) = show m+ show (Poly p) = show p+ show (Function a b) =+ let isForall (Forall _ _) = True+ isForall _ = False+ astr = if isFunction a || isForall a then "(" ++ show a ++ ")" else show a+ in astr ++ " -> " ++ show b+ show (Forall p expr) =+ let getQuant :: SystemF m p -> ([p], SystemF m p)+ getQuant (Forall _p _expr) = getQuant _expr & _1 %~ (_p :)+ getQuant _expr = ([], _expr)+ (ps, _expr) = getQuant expr+ in "forall " ++ unwords (show <$> (p:ps)) ++ ". " ++ show _expr+++deriveBifunctor ''SystemF+deriveBifoldable ''SystemF+deriveBitraversable ''SystemF+TH.deriveLift ''SystemF++instance (Ord m, Ord p) => SimpleType (SystemF m p) where++ type MonoType (SystemF m p) = m++ abstract = Function++ reify (Function a b) = Just (a, b)+ reify _ = Nothing++ bases = \case+ Function fun arg -> bases fun <> bases arg+ Forall p expr -> Set.insert (Poly p) (bases expr)+ expr -> Set.singleton expr++ mono = Mono++ equivalent = areAlphaEquivalent++instance (Ord m, Ord p) => Polymorphic (SystemF m p) where++ type PolyType (SystemF m p) = p++ substitutions =+ let (<><>) :: (Semigroup s1, Semigroup s2) => Either s1 s2 -> Either s1 s2 -> Either s1 s2+ (<><>) = curry $ \case+ (Left a, Left b) -> Left (a <> b)+ (a, b) -> (<>) <$> a <*> b+ in curry $ \case+ (Forall _ expr1 , expr2) -> substitutions expr1 expr2+ (expr1 , Forall _ expr2) -> substitutions expr1 expr2+ (Poly p1 , Poly p2) -> Right [Mutual p1 p2]+ (expr , Poly p) -> Right [Substitution expr p]+ (Poly p , expr) -> Right [Substitution expr p]+ (Function arg1 ret1, Function arg2 ret2) -> substitutions arg1 arg2 <><> substitutions ret1 ret2+ (expr1 , expr2)+ | expr1 == expr2 -> Right []+ | otherwise -> Left [(expr1, expr2)]++ applySubstitution sub target = applySubstitution' where+ applySubstitution' = \case+ m@Mono{} -> m+ p'@(Poly p)+ | p == target -> sub+ | otherwise -> p'+ Forall p expr+ | p == target -> applySubstitution' expr+ | otherwise -> Forall p (applySubstitution' expr)+ Function from to -> Function (applySubstitution' from) (applySubstitution' to)++ quantify = Forall++ poly = Poly++ quantifiedOf = \case+ Mono _ -> Set.empty+ Poly _ -> Set.empty+ Function from to -> quantifiedOf from <> quantifiedOf to+ Forall p texpr -> Set.insert (poly p) (quantifiedOf texpr)++ polytypesOf = \case+ Mono _ -> Set.empty+ p@Poly{} -> Set.singleton p+++{-|+ Error sum not within Eithers because those (GHC) type errors are messy.+-}+data SystemFErr c v t =+ SFNotKnownErr (NotKnownErr c v t)+ | SFSimpleTypeErr (SimpleTypeErr t)+ | SFSubsErr (SubsErr Gr t (PolyType t))++deriving instance (Polymorphic t, Eq v, Eq c) => Eq (SystemFErr c v t)+deriving instance (Polymorphic t, Show v, Show c, Show t, Show (PolyType t)) => Show (SystemFErr c v t)++data SystemFContext c v t p = SystemFContext {+ _polyctx :: SubsContext t p+ -- ^ The context for Polymorphic related information+ , _stlcctx :: SimpleTypingContext c v t+ -- ^ The context for Simply-typed related information.+} deriving (Eq, Ord, Show)++makeLenses ''SystemFContext++instance (Ord c, Ord v, Ord m, Ord p) => Typecheckable (LambdaTerm c v) (SystemF m p) where++ type TypingContext (LambdaTerm c v) (SystemF m p) = (SystemFContext c v (SystemF m p) p)++ type TypeError (LambdaTerm c v) (SystemF m p) =+ ErrorContext'+ (LambdaTerm c v)+ (SystemF m p)+ (SystemFErr c v (SystemF m p))++ typecheck env _expr = runTypecheck env (typecheck' _expr) where+ {-+ Using thhe+ -}+ typecheck' :: LambdaTerm c v (SystemF m p) -> Typecheck (LambdaTerm c v) (SystemF m p) (SystemF m p)+ typecheck' __expr =+ -- Append the current expression to any ErrorContexts+ flip catchError (throwError . fmap (expression %~ (__expr :)))+ $ case __expr of+ Variable v -> do+ -- Query the type of the variable+ t <- Map.lookup v <$> use (stlcctx.variables)+ -- Nameerror action in case v doesn't exist within the typing context.+ let nameErr = throwErrorContext [] (SFNotKnownErr (UnknownVariable v))+ -- If v's type (t) is Nothing then nameerror, otherwise just return it.+ maybe nameErr return t++ Constant c -> do+ -- Query the type of the constant+ t <- Map.lookup c <$> use (stlcctx.constants)+ -- Nameerror action in case c doesn't exist within the typing context.+ let nameErr = throwErrorContext [] (SFNotKnownErr (UnknownConstant c))+ -- If c's type (t) is Nothing then nameerror, otherwise just return it.+ maybe nameErr return t++ Apply fun arg -> do+ fun'type <- typecheck' fun+ arg'type <- typecheck' arg+ -- Split fun'type into it's components+ (fun'from, fun'to) <- case reify fun'type of+ -- fun'type wasn't a function type, throw an error.+ Nothing -> throwErrorContext [fun] (SFSimpleTypeErr (NotAFunction fun'type))+ -- return the result+ Just reified -> return reified+ case unify fun'from arg'type of+ Left errs ->+ -- If errors were encountered during unification, throw them.+ throwErrorContexts ((,) [] . SFSubsErr <$> errs)+ Right subs ->+ -- If substitutions were unified, then apply them to the+ -- return type of the function.+ return $ unvalidatedApplyAllSubs subs fun'to++ Lambda (v, t) expr -> do+ -- If there are any types in v's type expression that+ -- do not appear in the typing context or are not declated+ -- within it, throw errors for the unknown types.+ unknownTypes <- calcUnknownTypes t <$> use (stlcctx.allTypes)+ unless (null unknownTypes) (throwErrorContexts ((,) [] <$> unknownTypes))+ -- save the current state in scope+ oldstate <- get+ -- Register the variable v to have the type t in the current state+ -- and typecheck the lambda's body with that state.+ stlcctx.variables %= Map.insert v t+ -- Also register all the outmost declared poly types+ stlcctx.allTypes %= (outmostDeclaredPolys t <>)+ -- Typecheck the lambda's expression with this added information+ expr'type <- typecheck' expr+ -- Reset to the old state.+ put oldstate+ -- Return the type of this expression.+ return (t /-> expr'type)++ calcUnknownTypes t types =+ SFNotKnownErr . UnknownType <$> Set.toList (Set.difference (bases t) types)++ outmostDeclaredPolys (Forall p texpr) = Set.insert (poly p) (outmostDeclaredPolys texpr)+ outmostDeclaredPolys _ = Set.empty++instance (Ord m, Ord p, Arbitrary m, Data m, Arbitrary p, Data p) => Arbitrary (SystemF m p) where+ -- TODO: remove instances of Data for m and p+ arbitrary = process <$> sized (generatorSRWith aliases) where+ aliases :: [AliasR Gen]+ aliases = [+ aliasR (\() -> arbitrary :: Gen m)+ , aliasR (\() -> arbitrary :: Gen p)+ ]++ {-+ Remove all generated quantifications and then generalise the expression's poly types.+ -}+ process = generalise' . massUnquantify where+ {-+ Actually, remove all quantifications as we don't actually care about them during+ substitution, which is most of what's getting tested.++ Also SystemF doesn't do existential quantification by default (probably?)+ -}+ massUnquantify :: SystemF m p -> SystemF m p+ massUnquantify t@Mono{} = t+ massUnquantify t@Poly{} = t+ massUnquantify (Function from to) = massUnquantify from /-> massUnquantify to+ massUnquantify (Forall _ texpr) = massUnquantify texpr
+ src/Compiler/Typesystem/SystemFOmega.hs view
@@ -0,0 +1,155 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE UndecidableInstances #-}+{-|+ <https://en.wikipedia.org/wiki/System_F#System_F.CF.89 System Fω> is a System F that allows+ type operators (@Set Int@, @List Int@, @Either Int Bool@ etc.)+-}+module Compiler.Typesystem.SystemFOmega (+ SystemFOmega+ , markAsFunctionArrow+) where++import Calculi.Lambda+import Calculi.Lambda.Cube.HigherOrder+import Calculi.Lambda.Cube.Polymorphic+import Calculi.Lambda.Cube.SimpleType+import Control.Typecheckable+import Compiler.Typesystem.SimplyTyped (SimplyTyped)+import qualified Language.Haskell.TH.Lift as TH+import Data.Bifunctor.TH+import Data.Generics+import Data.Random.Generics+import Data.Semigroup+import qualified Data.Set as Set+import Test.QuickCheck++{-|+ A data type representing the components of System-Fω, with a parameterized+ higher-order typesystem @k@.+-}+data SystemFOmega m p k =+ Mono m+ -- ^ A mono type+ | FunctionArrow+ -- ^ Explicitly stated mono type of kind @(* → * → *)@ for type application reasons+ | Poly p+ -- ^ A poly type, i.e. the "@a@" in "@∀ a. a → a@"+ | Forall (p, k) (SystemFOmega m p k)+ -- ^ A binding of a poly type in a type expression, i.e. the "@∀ a.@" in "@∀ a. a@"+ | TypeAp (SystemFOmega m p k) (SystemFOmega m p k)+ -- ^ Type application.+ deriving (Eq, Ord, Show, Read, Data)++infixl 0 `TypeAp`++deriveBifunctor ''SystemFOmega+deriveBifoldable ''SystemFOmega+deriveBitraversable ''SystemFOmega+TH.deriveLift ''SystemFOmega++instance (Ord m, Ord p, Ord k) => SimpleType (SystemFOmega m p (Maybe k)) where+ -- SystemFOmega's mono type is it's type parameter 'm'+ type MonoType (SystemFOmega m p (Maybe k)) = m++ -- Making a function type from one type to another involves+ -- using type application on the function arrow.+ abstract a b = FunctionArrow `TypeAp` a `TypeAp` b++ reify (FunctionArrow `TypeAp` a `TypeAp` b) = Just (a, b)+ reify _ = Nothing++ bases = \case+ Forall _ sf -> bases sf+ TypeAp tl tr -> bases tl `Set.union` bases tr+ a -> Set.singleton a++ mono = Mono++ equivalent = areAlphaEquivalent++instance (Ord m, Ord p, Ord k) => Polymorphic (SystemFOmega m p (Maybe k)) where++ type PolyType (SystemFOmega m p (Maybe k)) = p++ substitutions = curry $ \case+ (Forall _ expr1 , expr2) -> substitutions expr1 expr2+ (expr1 , Forall _ expr2) -> substitutions expr1 expr2+ (Poly p1 , Poly p2) -> Right [Mutual p1 p2]+ (expr , Poly p) -> Right [Substitution expr p]+ (Poly p , expr) -> Right [Substitution expr p]+ (TypeAp arg1 ret1 , TypeAp arg2 ret2) -> substitutions arg1 arg2 <><> substitutions ret1 ret2+ (expr1 , expr2)+ | expr1 == expr2 -> Right []+ | otherwise -> Left [(expr1, expr2)]++ applySubstitution sub target = applySubstitution' where+ applySubstitution' = \case+ m@Mono{} -> m+ FunctionArrow -> FunctionArrow+ p'@(Poly p)+ | p == target -> sub+ | otherwise -> p'+ Forall declr@(p, _) sf+ | p == target -> applySubstitution' sf+ | otherwise -> Forall declr (applySubstitution' sf)+ TypeAp tl tr -> TypeAp (applySubstitution' tl) (applySubstitution' tr)++ quantify = Forall . flip (,) Nothing++ poly = Poly++ quantifiedOf = \case+ Forall (p, _) texpr -> Set.insert (poly p) $ quantifiedOf texpr+ TypeAp texpr1 texpr2 -> quantifiedOf texpr1 <> quantifiedOf texpr2+ _ -> Set.empty++instance (+ Ord m+ , Ord p+ , Ord k+ , Inferable (SystemFOmega m p) k+ , TypingContext (SystemFOmega m p) k ~ InferenceContext (SystemFOmega m p) k)+ => HigherOrder (SystemFOmega m p (Maybe k)) where+ type Kindsystem (SystemFOmega m p (Maybe k)) = k++ type KindError (SystemFOmega m p (Maybe k)) =+ Either (InferError (SystemFOmega m p) k)+ (TypeError (SystemFOmega m p) k)++ type KindContext (SystemFOmega m p (Maybe k)) = (TypingContext (SystemFOmega m p) k)++ kindcheck env texpr = case infer env texpr of+ Left errs -> Left (Left <$> errs)+ Right (env', texpr') -> case typecheck env' texpr' of+ Left errs -> Left (Right <$> errs)+ Right (env'', texpr'') -> Right (env'', texpr'')++ typeap = TypeAp++ untypeap (TypeAp a b) = Just (a, b)+ untypeap _ = Nothing++instance (Data m, Data p, Data k, Arbitrary m, Arbitrary p, Arbitrary k) => Arbitrary (SystemFOmega m p k) where+ -- TODO: remove instances of Data for m and p+ arbitrary = sized (generatorSRWith aliases) where+ aliases :: [AliasR Gen]+ aliases = [+ aliasR (\() -> arbitrary :: Gen m)+ , aliasR (\() -> arbitrary :: Gen p)+ ]++{-|+ Given a function arrow representation of type @m@, replace all+ matching mono types with the function arrow.+-}+markAsFunctionArrow :: Eq m => m -> SystemFOmega m p k -> SystemFOmega m p k+markAsFunctionArrow sub = \case+ m@(Mono x)+ | x == sub -> FunctionArrow+ | otherwise -> m+ FunctionArrow -> FunctionArrow+ p@Poly{} -> p+ Forall p st -> Forall p (markAsFunctionArrow sub st)+ TypeAp t1 t2 -> TypeAp (markAsFunctionArrow sub t1) (markAsFunctionArrow sub t2)
+ src/Control/Typecheckable.hs view
@@ -0,0 +1,148 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-|+ Module containing typechecking functions and data structures.++-}+module Control.Typecheckable (+ -- * Typeclasses for Typechecking and Inference+ Typecheckable(..)+ , Inferable(..)+ -- * Typing context and Type error structures+ -- ** General use+ , Typecheck+ , runTypecheck+ , expression+ , environment+ , (<><>)+ -- ** ErrorContext+ , ErrorContext(..)+ , ErrorContext'+ , throwErrorContext+ , throwErrorContexts+ , errorOfContext+ , appendExprToEContexts+) where++import Data.Bifunctor+import Control.Monad.State+import Control.Monad.Except+import Data.Semigroup+import qualified Data.Map as Map+import qualified Data.Set as Set+import qualified Data.List.NonEmpty as NE+import Control.Lens+import Data.Tree as Tree++{-|+ Data type for an error context, holding the expression where+ the error occurred, the environment when it did, and the error+ itself.+-}+data ErrorContext env expr err = ErrorContext {+ _expression :: [expr]+ -- ^ A stack of expressions leading the the expression that+ -- caused the error as the final element.+ , _environment :: env+ -- ^ The environment's state at the time of error.+ , _errorOfContext :: err+ -- ^ The error that occurred.+} deriving (Eq, Ord, Show)++makeLenses ''ErrorContext++{-|+ ErrorContext but the environment is assumed to be the TypingContext of @t@.+-}+type ErrorContext' term t err = ErrorContext (TypingContext term t) (term t) err++instance Functor (ErrorContext env expr) where+ fmap f = errorOfContext %~ f++{-|+ Throw an error in an 'ErrorContext'.+-}+throwErrorContext exprStack err = throwErrorContexts [(exprStack, err)]++{-|+ Throw a list of errors in `ErrorContext`'s.+-}+throwErrorContexts exprsAndErrs = do+ -- Get the current environment at the time of the errors.+ env <- get+ -- For every error, create an ErrorContext with the environment 'env' and the given error+ -- error and expression stack.+ throwError ((\(exprStack, err) -> ErrorContext exprStack env err) <$> exprsAndErrs)++{-|+ If there have been any errors, add the given expression to the head of+ all the error contexts' expression stacks.+-}+appendExprToEContexts expr = flip catchError (throwError . fmap (expression %~ (expr :)))++{-|+ A validation semigroup on Eithers, combining Left values when two appear.+-}+(<><>) :: (Semigroup s1, Semigroup s2) => Either s1 s2 -> Either s1 s2 -> Either s1 s2+(<><>) = curry $ \case+ (Left a, Left b) -> Left (a <> b)+ (a, b) -> (<>) <$> a <*> b++{-|+ Typechecking type, uses the TypingContext as state and TypeError as an exception type.+-}+type Typecheck term t = ExceptT [TypeError term t] (State (TypingContext term t))++-- | runs a `Typecheck` action+runTypecheck :: st -> ExceptT e (State st) t -> Either e (st, t)+runTypecheck env = (\(e, st) -> (,) st <$> e ) . flip runState env . runExceptT++{-|+ A typeclass for typechecking terms (@term@) with a typesystem (@t@).+-}+class Typecheckable (term :: * -> *) t where+ {-|+ The typing context, in type theory this is usually shown as 𝚪.++ For a basic typechecker of the simply-typed lambda calculus this might contain+ a mapping of variable and constant names to their types. This is left to be defined+ for the implementer though as other typesystems might need extra information+ in their contexts.+ -}+ type TypingContext term t :: *++ {-|+ The type error representation.+ -}+ type TypeError term t :: *++ {-|+ Given a typing context, typecheck an expression and either return a typeerror or the+ type of the expression that was passed.+ -}+ typecheck :: TypingContext term t -- ^ The given context+ -> term t -- ^ The expression to typecheck+ -> Either [TypeError term t]+ (TypingContext term t, t) -- ^ The result++class (Typecheckable term t) => Inferable term t where++ {-|+ The inference context, has a similar function to `TypingContext`+ -}+ type InferenceContext term t :: *++ {-|+ The inference error representation.+ -}+ type InferError term t :: *++ infer :: InferenceContext term t -- ^ The given context+ -> term (Maybe t) -- ^ The expression to infer from+ -> Either [InferError term t]+ (InferenceContext term t, term t) -- ^ The result++ {-|+ Get a typing context from an inference context.+ -}+ typingContext :: InferenceContext term t -> TypingContext term t
+ src/Data/Graph/Inductive/Helper.hs view
@@ -0,0 +1,126 @@+module Data.Graph.Inductive.Helper where++import Data.Graph.Inductive as Graph+import qualified Data.Map as Map+import Data.Maybe+import qualified Data.Set as Set+import qualified Data.Tree as Tree+import Safe++findRootPaths :: Graph gr => gr n e -> Graph.Context n e -> (Node, [[Node]])+findRootPaths = findRootPathsBy (\(_, node, _, _) -> node)++findRootPathsBy :: Graph gr => (Graph.Context n e -> a) -> gr n e -> Graph.Context n e -> (a, [[a]])+findRootPathsBy f graph ctx = (f ctx, findRootPathsRec [] ctx) where+ findRootPathsRec path ctx'@(inward, _, _, _) = case inward of+ [] -> [f ctx' : path]+ a -> concatMap (findRootPathsRec (f ctx' : path) . context graph . snd) a++treeRootStatefulBy+ :: Graph gr+ => (st -> Graph.Context n e -> (a, st)) -- ^ The stateful fold function+ -> st -- ^ The initial state+ -> gr n e -- ^ The graph to traverse+ -> Graph.Context n e -- ^ The initial context+ -> Tree.Tree (a, st) -- ^ The resulting tree of values and states at each node.+treeRootStatefulBy f st graph = trsbRec st where+ trsbRec st' ctx'@(inward, _, _, _) =+ let val = f st' ctx'+ in Tree.Node val (trsbRec (snd val) . context graph . snd <$> inward)++cyclesOfGraph :: Graph gr => gr n l -> [[LNode n]]+cyclesOfGraph graph = fromMaybe [] -- give a default to bring this out of the Maybe+ . sequence -- sequence again from [Maybe [...]] to Maybe [[...]]+ . fmap -- construct lnodes from each bare node+ ( sequence -- sequence from [Maybe ...] t0 Maybe [...]+ . fmap (\n -> (,) n <$> lab graph n)) -- make the lnode from the node+ . filter hasSome -- filter out any with only 1 element+ . scc $ graph -- get the strongly connected components++{-|+ Given a graph, generate a possibly empty list of subgraphs that are the it's cycles.+-}+cyclicSubgraphs :: forall gr n e. (DynGraph gr, Ord n, Ord e) => gr n e -> [gr n e]+cyclicSubgraphs graph = flip subgraph graph <$> filter hasSomeLI (scc graph) where+ -- hasSome but is inclusive of loops (nodes with edges to itself)+ hasSomeLI :: [Node] -> Bool+ hasSomeLI [] = False+ hasSomeLI [n] = not . null $ filter (\(n1,n2,_) -> n == n1 && n1 == n2) (out graph n ++ inn graph n)+ hasSomeLI _ = True++-- | Returns true if a list has more than 1 element+hasSome :: [a] -> Bool+hasSome [] = False+hasSome [_] = False+hasSome _ = True++-- | Returns true if a list of contexts has more than one element or a loop in it's only element.+hasSome' :: [Graph.Context n l] -> Bool+hasSome' [] = False+hasSome' [(_, noden, _, outward)] = any ((== noden) . snd) outward+hasSome' _ = True++{-|+ Build a graph with no edges from a foldable container of node values.+-}+buildFromNodes :: (DynGraph gr, Foldable t) => t a -> gr a ()+buildFromNodes =+ fst . foldr (\n (gr, h : tl) -> (([], h, n, []) & gr, tl)) (Graph.empty, [(0 :: Node)..])++{-|+ A version of topsort that returns cycles as groups rather than+ incorperating them into it's result arbitrarily.++ It's result is a list of eithers, with Left values representing+ cycles and Right values as nodes not within a cycle, in an order+ similar to what is given by a regular topsort.+-}+topsortWithCycles :: (Graph gr, Ord a) => gr a b -> [Either [a] a]+topsortWithCycles graph =+ let+ -- Map of all nodes that are within a cycle to the cycle they are a member of.+ -- Given the cycle finding function uses fgl's strongly connected components+ -- function, there should be no nodes that exist in more than one cycle.+ cycleMap = Map.fromList . concat $ (\cy -> zip cy (repeat (Set.fromList cy))) . fmap snd <$> cyclesOfGraph graph+ -- Get the initial topsort.+ tsorted = topsort' graph+ -- Crummy hack to sieve out cycles as they appear in the topsort result+ sieveCycles [] = []+ sieveCycles (h : tl) = case Map.lookup h cycleMap of+ Nothing -> Right h : sieveCycles tl+ Just cy -> Left (Set.toList cy) : sieveCycles (filter (`Set.notMember` cy) tl)+ in sieveCycles tsorted++{-|+ Convert a tree into a list of all of it's paths.+-}+treeToPaths :: Tree.Tree a -> [[a]]+treeToPaths (Tree.Node l []) = [[l]]+treeToPaths (Tree.Node l sbf) = (l :) <$> concat (treeToPaths <$> sbf)++{-|+ Build a topsort inclusive of outward edges. Nodes without outward edges+ are ignored.++ If there are cycles in the graph, Nothing is returned.+-}+edgeyTopsort :: Graph gr => gr n e -> Maybe [(n, e)]+edgeyTopsort graph+ | not (null (cyclesOfGraph graph)) = Nothing+ | otherwise = Just (unvalidatedEdgeyTopsort graph)++{-|+ `edgeyTopsort` but doesn't check for cycles first.+-}+unvalidatedEdgeyTopsort :: Graph gr => gr n e -> [(n, e)]+unvalidatedEdgeyTopsort graph =+ {-+ In a cycle-less graph, there should always be 1 node+ that has no inward edge. If there's not, then we've+ finished the topsort+ -}+ let candidate = headMay $ gsel (null . inn') graph+ in case flip match graph . node' <$> candidate of+ Nothing -> []+ Just (Nothing, _) -> []+ Just (Just ctx, graph') -> fmap (\(_, _, l) -> (lab' ctx, l)) (out' ctx) ++ unvalidatedEdgeyTopsort graph'
+ test/Spec.hs view
@@ -0,0 +1,173 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE DeriveDataTypeable #-}+import Calculi.Lambda+import Calculi.Lambda.Cube+import Calculi.Lambda.Cube.Polymorphic+import Calculi.Lambda.Cube.Polymorphic.Unification+import Compiler.Typesystem.SimplyTyped as ST+import Compiler.Typesystem.SystemF as SF+import Compiler.Typesystem.SystemFOmega as SFO+import Data.Maybe+import Data.Generics+import Data.Semigroup+import Control.Arrow hiding (first, second)+import Data.Either.Combinators+import Data.Bifunctor+import Debug.Trace+import qualified Data.Set as Set+import Test.Hspec+import Test.Hspec.QuickCheck+import Test.QuickCheck++main :: IO ()+main = hspec $ do+ describe "Type systems follow laws and properties" $ do+ describe "SimplyTyped" $+ followsSimpleType (arbitrary :: Gen SimplyTyped')+ describe "System-F" $ do+ followsSimpleType (arbitrary :: Gen SystemF')+ followsPolymorphic (arbitrary :: Gen SystemF')+ describe "System-Fω" $ do+ followsSimpleType (arbitrary :: Gen SystemFOmega')+ followsPolymorphic (arbitrary :: Gen SystemFOmega')+ followsHigherOrder (arbitrary :: Gen SystemFOmega')++ unificationRules (arbitrary :: Gen SystemF')++type SimplyTyped' = SimplyTyped AlphabetUpper+type SystemFOmega' = SystemFOmega AlphabetUpper AlphabetLow+type SystemF' = SF.SystemF AlphabetUpper AlphabetLow++followsSimpleType :: forall t. (SimpleType t, Show t, Arbitrary t) => Gen t -> Spec+followsSimpleType gen = describe "SimpleType laws and properties" $ do+ prop "equivalence is reflexive" $ ((\ !ty -> ty ==== ty) :: t -> Bool)+ prop "follows abstract-reify inverse law" $ (abstractInverse :: t -> t -> Bool)++followsPolymorphic :: forall t.+ (+ Polymorphic t+ , Show t+ , Arbitrary t+ , Arbitrary (PolyType t)+ , Show (PolyType t)+ , Enum (PolyType t)+ )+ => Gen t -> Spec+followsPolymorphic gen = describe "Polymorphic laws and properties" $ do+ prop "follows type-ordering rule ((forall a. a) ⊑ _ = True)"+ (typeOrderingRule :: t -> Bool)+ prop "lifts up quantification during abstraction"+ (liftQuantifiersRule :: t -> PolyType t -> Bool)++unificationRules :: forall t.+ (+ Polymorphic t+ , Show t+ , Arbitrary t+ , Arbitrary (PolyType t)+ , Show (PolyType t)+ , Enum (PolyType t)+ )+ => Gen t -> Spec+unificationRules _ = describe "Unification rules and properties" $ do+ modifyMaxSuccess (* 20) $ prop "follows unification rule: when U(t, t') = V; V(t) ≣ V(t')" $+ forAll (arbitrary' `suchThat` unifyR1Predicate)+ (uncurry unifyR1 :: ((t, t) -> Bool))+ modifyMaxSuccess (* 5) $ prop "follows unification rule: when U(t, t') = V; ftvs(V(t) ∪ V(t')) ⊂ (ftvs(t) ∪ ftvs(t'))" $+ forAll (arbitrary' `suchThat` unifyR1Predicate)+ (uncurry unifyR2 :: ((t, t) -> Bool))+ where+ {-+ Tweaked random generator that includes some type expressions that+ might make failing cases appear more frequently than if they were+ just generated by the Arbitrary instance itself.+ -}+ arbitrary' :: Gen (t, t)+ arbitrary' = frequency [(9, arbitrary), (1, endomorphism)] where+ -- Endomorphisms (type expressions of the form "forall a. a -> a")+ -- paired with a type expression generaed with the regular+ -- Arbitrary instance.+ endomorphism = do+ tvar <- arbitrary :: Gen (PolyType t)+ l <- arbitrary :: Gen t+ return (l, quantify tvar (poly tvar /-> poly tvar))++followsHigherOrder :: forall t. (Show t, HigherOrder t, Arbitrary t) => Gen t -> Spec+followsHigherOrder gen = describe "HigherOrder laws and properties" $ do+ prop "follows typeap-untypeap inverse law" $ (typeapInverse :: t -> t -> Bool)++{-|+ Check that `reify` is the inverse (within a Maybe) of `abstract`.+-}+abstractInverse :: (SimpleType t) => t -> t -> Bool+abstractInverse !ta !tb = fmap (uncurry (/->)) (reify (ta /-> tb)) == Just (ta /-> tb)+++typeapInverse :: HigherOrder t => t -> t -> Bool+typeapInverse !ta !tb = fmap (uncurry (/$)) (untypeap (ta /$ tb)) == Just (ta /$ tb)++typeOrderingRule :: (Enum e, Polymorphic t, PolyType t ~ e) => t -> Bool+typeOrderingRule !t = poly (toEnum 9999) ⊑ t++{-+ Assert that `abstract` lifts all of the quantifiers to the result.+-}+liftQuantifiersRule :: (Polymorphic t, PolyType t ~ p) => t -> p -> Bool+liftQuantifiersRule t p = t /-> quantify p (poly p) == quantify p (t /-> poly p)++unifyR1 :: forall t e. (Enum e, Polymorphic t, Show t, PolyType t ~ e) => t -> t -> Bool+unifyR1 !t1 !t2 =+ -- If the unification returns errors, then return true as+ -- this rule is checking the property itself, not the substitution errors.+ fromRight True $ do+ subs <- unify t1 t2+ u <- applyAllSubsGr subs+ return (u t1 ==== u t2)++unifyR2 !t1 !t2 =+ fromRight True $ do+ subs <- unify t1 t2+ u <- applyAllSubsGr subs+ return $+ (bases (u t1) <> bases (u t2)) `Set.isSubsetOf` (bases t1 <> bases t2)++{-+ The input predicate for unifyR1; the type variables in each expression+ must be disjoint, there must be valid substitutions between the two expressions,+ and the expressions must not be equivalent to eachother.+-}+unifyR1Predicate (t1, t2) =+ t1'tvs `disjoint` t2'tvs && hasSubstitutions t1 t2 && not (t1 ==== t2) where+ t1'tvs = polytypesOf t1+ t2'tvs = polytypesOf t2++disjoint a b = Set.difference a b == a++newtype AlphabetLow = AlphabetLow Integer deriving (Eq, Ord, Enum, Data, Typeable)++instance Arbitrary AlphabetLow where+ arbitrary = AlphabetLow <$> elements [0..35]++instance Show AlphabetLow where+ show (AlphabetLow n) = char : if suffix == 0 then+ "" else show suffix where+ suffix = (n - charNum) `div` 36++ charNum = n `mod` 36++ char = (cycle ['a'..'z']) !! fromEnum charNum++newtype AlphabetUpper = AlphabetUpper Integer deriving (Eq, Ord, Enum, Data, Typeable)++instance Arbitrary AlphabetUpper where+ arbitrary = AlphabetUpper <$> elements [0..35]++instance Show AlphabetUpper where+ show (AlphabetUpper n) = char : if suffix == 0 then "" else (show suffix) where+ suffix = (n - charNum) `div` 36++ charNum = n `mod` 36++ char = (cycle ['A'..'Z']) !! fromEnum charNum
+ typerbole.cabal view
@@ -0,0 +1,109 @@+name: typerbole+version: 0.0.0.1+synopsis: A typeystems library with exaggerated claims+description: Please see README.md+license: BSD3+license-file: LICENSE+author: Fionan Haralddottir+maintainer: ma302fh@gold.ac.uk+copyright: 2016 Fionan Haralddottir+category: Typesystems+ , Typechecking+ , TypeTheory+ , Educational+ , LambdaCube+ , AST+build-type: Simple+cabal-version: >=1.10+extra-source-files: README.md+ , lambdacube-overview.md+ , diagrams/typeclass-hierarchy.png+ , CONTRIBUTING.md++library+ hs-source-dirs: src+ exposed-modules: Calculi.Lambda+ , Calculi.Lambda.Cube+ , Calculi.Lambda.Cube.SimpleType+ , Calculi.Lambda.Cube.Polymorphic+ , Calculi.Lambda.Cube.Polymorphic.Unification+ , Calculi.Lambda.Cube.HigherOrder+ , Calculi.Lambda.Cube.Dependent+ , Calculi.Lambda.Cube.TH+ , Compiler.Typesystem.Hask+ , Compiler.Typesystem.SystemF+ , Compiler.Typesystem.SystemFOmega+ , Compiler.Typesystem.SimplyTyped+ , Control.Typecheckable+ , Data.Graph.Inductive.Helper+ build-depends: base >= 4.7 && < 5+ , containers >= 0.5 && < 0.6+ , data-ordlist+ , either+ , semigroups+ , bifunctors >= 5+ , fgl >= 5.5 && < 5.6+ , QuickCheck+ , syb+ , mtl+ , generic-random == 0.1.1.0+ , lens+ , template-haskell+ , th-lift+ , megaparsec+ , safe+ ghc-options: -Wall+ -fno-warn-type-defaults+ -fno-warn-unused-do-bind+ default-language: Haskell2010+ default-extensions: ScopedTypeVariables+ , LambdaCase+ , TemplateHaskell+ , DeriveGeneric+ , DeriveDataTypeable+ , TypeFamilies+ , QuasiQuotes+ , TypeOperators+ , MultiParamTypeClasses+ , FunctionalDependencies+++test-suite typerbole-testing+ type: exitcode-stdio-1.0+ hs-source-dirs: test+ main-is: Spec.hs+ build-depends: base+ , QuickCheck+ , hspec+ , checkers+ , typerbole+ , containers+ , bifunctors >= 5 && < 5.3+ , either+ , semigroups+ , syb+ ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall+ default-language: Haskell2010+ default-extensions: ScopedTypeVariables+ , LambdaCase+ , TemplateHaskell+ , DeriveGeneric+ , TypeFamilies++-- Executable to generate vector graphics related to this+-- project.+executable typerbole-diagrams+ hs-source-dirs: diagrams+ main-is: Main.hs+ build-depends: base+ , diagrams-lib+ , diagrams-svg+ , colour+ ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall+ default-language: Haskell2010+ default-extensions: ScopedTypeVariables+ , LambdaCase+ , NoMonomorphismRestriction+ , TemplateHaskell+ , DeriveGeneric+ , TypeFamilies