[WIP] Pairs

.gitignore

@@ -1,3 +1,3 @@
 .DS_Store
 .stack-work
-
+tags

Surface.cabal

@@ -23,8 +23,11 @@ library
                      , Data.Term
                      , Data.Term.Types
                      , Data.Typing
-                     , Data.Unification
                      , Surface
+                     , Surface.Language
+                     , Surface.Pair
+                     , Surface.Renaming
+                     , Surface.Unification
   build-depends:       base >= 4.7 && < 5
                      , containers
   default-language:    Haskell2010
@@ -44,6 +47,8 @@ test-suite Surface-test
   main-is:             Spec.hs
   other-modules:       Data.Name.Internal.Spec
                      , Data.Term.Spec
+                     , Surface.Language.Spec
+                     , Surface.Pair.Spec
                      , Test.Assertions
   build-depends:       base
                      , Surface

src/Data/Expression.hs

@@ -1,15 +1,7 @@
 {-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
 module Data.Expression where
 
-import Data.Unification
-
 data Expression recur
   = Application recur recur
   | Lambda recur recur
   deriving (Functor, Show, Eq, Foldable, Traversable)
-
-instance Unifiable Expression where
-  unifyBy f expected actual = case (expected, actual) of
-    (Application a1 b1, Application a2 b2) -> Just $ Application (f a1 a2) (f b1 b2)
-    (Lambda a1 b1, Lambda a2 b2) -> Just $ Lambda (f a1 a2) (f b1 b2)
-    _ -> Nothing

src/Data/Module.hs

@@ -1,7 +1,17 @@
+{-# LANGUAGE FlexibleContexts #-}
 module Data.Module where
 
-import Data.Expression
+import qualified Data.List as List
 import Data.Term.Types
-import qualified Data.Map as Map
+import Surface.Language
 
-data Module = Module (Map.Map String (Term Expression))
+(!) :: Module term -> String -> Definition term
+Module definitions ! key = case List.find ((== key) . symbol) definitions of
+  Just x -> x
+  _ -> error "Expected definition to exist"
+
+checkModule :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Context (Term f) -> Module (Term f) -> Result [Term f]
+checkModule context (Module definitions) = sequence $ checkDefinition context <$> definitions
+
+checkDefinition :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Context (Term f) -> Definition (Term f) -> Result (Term f)
+checkDefinition context (Definition symbol t v) = typeOf t _type' context >> typeOf v t context

src/Data/Term.hs

@@ -5,7 +5,8 @@ import Data.Binding
 import Data.Name
 import Data.Typing
 import Data.Term.Types
-import Data.Unification
+import Surface.Renaming
+import Surface.Unification
 import qualified Data.Map as Map
 import qualified Data.Set as Set
 
@@ -21,9 +22,11 @@ abstract f = abstraction name scope
         name = maybe (Local 0) prime $ maxBoundVariable (f $ variable (Local $ negate 1))
 
 -- | Construct the annotation of a term by a type. The term will be checked against this type.
-annotation :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Term f -> Term f -> Term f
+annotation :: Foldable f => Term f -> Term f -> Term f
 annotation term type' = checkedTyping typeChecker $ Annotation term type'
-  where typeChecker against context = typeOf term type' context >>= expectUnifiable against
+  where typeChecker against context = do
+          _ <- typeOf term type' context
+          typeOf term against context
 
 
 checkedAbstraction :: Name -> Checker (Term f) -> Term f -> Term f
@@ -44,18 +47,9 @@ checkedBinding typeChecker = checkedTyping typeChecker . Binding
 checkedExpression :: Foldable f => Checker (Term f) -> f (Term f) -> Term f
 checkedExpression typeChecker = checkedBinding typeChecker . Expression
 
-_type :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Int -> Term f
-_type n = Term mempty (checkInferred $ const $ Right (_type (n + 1))) $ Type n
-
-_type' :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Term f
-_type' = _type 0
-
 implicit :: Term f
 implicit = Term mempty (const . Right) Implicit
 
-expectUnifiable :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Term f -> Term f -> Result (Term f)
-expectUnifiable expected actual = maybe (Left $ "error: Unification failed.\nExpected: '" ++ show expected ++ "'\n  Actual: '" ++ show actual ++ "'.\n") Right $ unified $ unify expected actual
-
 checkInferred :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Inferer (Term f) -> Checker (Term f)
 checkInferred inferer expected context = do
   actual <- inferer context
@@ -71,28 +65,6 @@ maxBoundVariable = cata $ \ t -> case t of
   Binding (Expression e) -> maximum e
   _ -> Nothing
 
-rename :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Name -> Name -> Term f -> Term f
-rename old new (Term freeVariables typeChecker typing) = Term (replace old new freeVariables) typeChecker $ renameTypingBy (rename old new) old new typing
-
-replace :: Ord a => a -> a -> Set.Set a -> Set.Set a
-replace old new set = if Set.member old set then Set.insert new $ Set.delete old set else set
-
-renameUnification :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Name -> Name -> Unification f -> Unification f
-renameUnification old new (Unification freeVariables out) = Unification (replace old new freeVariables) $ renameTypingBy (renameUnification old new) old new out
-renameUnification old new (Conflict expected actual) = Conflict (rename old new expected) (rename old new actual)
-
-renameTypingBy :: Functor f => (g f -> g f) -> Name -> Name -> Typing (Binding f) (g f) -> Typing (Binding f) (g f)
-renameTypingBy _ old new typing | old == new = typing
-renameTypingBy f old new typing = case typing of
-  Binding (Variable name) -> if name == old then Binding (Variable new) else typing
-  Binding (Abstraction name scope) -> if name == old then typing else Binding $ Abstraction name (f scope)
-  Binding (Expression body) -> Binding $ Expression $ f <$> body
-
-  Annotation a b -> Annotation (f a) (f b)
-
-  Type _ -> typing
-  Implicit -> typing
-
 substitute :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Name -> Term f -> Term f -> Term f
 substitute name with term | with == variable name = term
 substitute name with term@(Term _ typeChecker binding) = case binding of
@@ -129,32 +101,3 @@ cata f = f . fmap (cata f) . out
 para :: Functor f => (Typing (Binding f) (Term f, a) -> a) -> Term f -> a
 para f = f . fmap fanout . out
   where fanout a = (a, para f a)
-
-byUnifying :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Checker (Term f) -> Checker (Term f) -> Checker (Term f)
-byUnifying a b against context = do
-  a' <- a against context
-  b' <- b against context
-  maybe (Left "couldn’t unify") Right $ unified $ unify a' b'
-
-unify :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Term f -> Term f -> Unification f
-unify expected actual = case (out expected, out actual) of
-  (a, b) | a == b -> into expected
-
-  (_, Implicit) -> into expected
-  (Implicit, _) -> into actual
-
-  (Type _, Type _) -> into expected
-  (Annotation term1 type1, Annotation term2 type2) -> Unification free (Annotation (unify term1 term2) (unify type1 type2))
-
-  (Binding (Abstraction name1 scope1), Binding (Abstraction name2 scope2)) | name1 == name2 -> Unification free (Binding $ Abstraction name1 (unify scope1 scope2))
-  (Binding (Abstraction name1 scope1), Binding (Abstraction name2 scope2)) -> Unification (Set.delete name1 free) (Binding $ Abstraction name1 (renameUnification name name1 (unify (rename name1 name scope1) (rename name2 name scope2))))
-    where name = pick free
-          free = freeVariables scope1 `Set.union` freeVariables scope2
-
-  (Binding (Abstraction name scope), _) | Set.notMember name (freeVariables scope) -> unify scope actual
-  (_, Binding (Abstraction name scope)) | Set.notMember name (freeVariables scope) -> unify expected scope
-
-  (Binding (Expression e1), Binding (Expression e2)) | Just e <- unifyBy unify e1 e2 -> Unification free $ Binding $ Expression e
-
-  _ -> Conflict expected actual
-  where free = freeVariables expected `Set.union` freeVariables actual

src/Data/Term/Types.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE StandaloneDeriving, UndecidableInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
 module Data.Term.Types where
 
 import Data.Binding
@@ -9,35 +9,48 @@ import qualified Data.Set as Set
 
 type Result a = Either String a
 
+data Module term = Module [Definition term]
+data Definition term = Definition { symbol :: String, getType :: term, getValue :: term }
+
 type Context term = Map.Map Name term
+type Environment term = Map.Map Name term
 
 type Inferer term = Context term -> Result term
 type Checker term = term -> Context term -> Result term
 
 data Term f = Term { freeVariables :: Set.Set Name, typeOf :: Checker (Term f), out :: Typing (Binding f) (Term f) }
 
-data Unification f = Unification (Set.Set Name) (Typing (Binding f) (Unification f)) | Conflict (Term f) (Term f)
+data Unification f = Unification (Set.Set Name) (Checker (Term f)) (Typing (Binding f) (Unification f)) | Conflict (Term f) (Term f)
+
+class Unifiable e where
+  unifyBy :: (f e -> f e -> Unification e) -> e (f e) -> e (f e) -> Maybe (e (Unification e))
 
 expected :: Functor f => Unification f -> Term f
 expected (Conflict expected _) = expected
-expected (Unification freeVariables out) = Term freeVariables (const . const $ Left "Unification does not preserve typecheckers.\n") (expected <$> out)
+expected (Unification freeVariables typeChecker out) = Term freeVariables typeChecker (expected <$> out)
 
 actual :: Functor f => Unification f -> Term f
 actual (Conflict _ actual) = actual
-actual (Unification freeVariables out) = Term freeVariables (const . const $ Left "Unification does not preserve typecheckers.\n") (actual <$> out)
+actual (Unification freeVariables typeChecker out) = Term freeVariables typeChecker (actual <$> out)
 
 unified :: Traversable f => Unification f -> Maybe (Term f)
 unified (Conflict _ _) = Nothing
-unified (Unification freeVariables out) = do
+unified (Unification freeVariables typeChecker out) = do
   out <- mapM unified out
-  return $ Term freeVariables (const . const $ Left "Unification does not preserve typecheckers.\n") out
+  return $ Term freeVariables typeChecker out
 
 into :: Functor f => Term f -> Unification f
-into term = Unification (freeVariables term) $ into <$> out term
+into term = Unification (freeVariables term) (typeOf term) $ into <$> out term
 
 
 instance Eq (f (Term f)) => Eq (Term f) where
   a == b = freeVariables a == freeVariables b && out a == out b
 
-deriving instance (Eq (Term f), Eq (f (Unification f))) => Eq (Unification f)
-deriving instance (Show (Term f), Show (f (Unification f))) => Show (Unification f)
+instance (Eq (Term f), Eq (f (Unification f))) => Eq (Unification f) where
+  (Unification freeVariablesA _ outA) == (Unification freeVariablesB _ outB) = freeVariablesA == freeVariablesB && outA == outB
+  (Conflict a1 b1) == (Conflict a2 b2) = a1 == a2 && b1 == b2
+  _ == _ = False
+
+instance (Functor f, Show (Term f), Show (f (Unification f))) => Show (Unification f) where
+  show u = "Expected: " ++ show (expected u) ++ "\n"
+        ++ "  Actual: " ++ show (actual u) ++ "\n"

src/Surface.hs

@@ -1,119 +1,14 @@
-{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
 module Surface (
   module Surface',
-  lambda,
-  Surface.pi,
-  (-->),
-  apply,
-  checkHasFunctionType,
-  checkIsFunctionType,
-  checkIsType,
 ) where
 
-import Prelude hiding (pi)
 import Data.Binding as Surface'
 import Data.Expression as Surface'
+import Data.Module as Surface'
 import Data.Name as Surface'
-import Data.Name.Internal
 import Data.Term as Surface'
 import Data.Term.Types as Surface'
 import Data.Typing as Surface'
-import Data.Unification as Surface'
-import Control.Applicative
-import qualified Data.Set as Set
-
-infixr `lambda`
-
--- | Construct a lambda from a type and a function from an argument variable to the resulting term. The variable will be picked automatically. The parameter type will be checked against `Type`, but there are no constraints on the type of the result.
-lambda :: Term Expression -> (Term Expression -> Term Expression) -> Term Expression
-lambda t f = checkedExpression checkType $ Lambda t body
-  where body = abstract f
-        checkType expected context = case out expected of
-          Binding (Expression (Lambda from to)) -> checkTypeAgainst from to context
-          Type _ -> checkTypeAgainst _type' _type' context
-          _ -> checkTypeAgainst implicit implicit context >>= expectUnifiable expected
-        checkTypeAgainst from to context = do
-          _ <- checkIsType t context
-          _ <- expectUnifiable from t
-          bodyType <- inferTypeOf body (extendContext t context body)
-          _ <- expectUnifiable to bodyType
-          return $ case shadowing body bodyType of
-            Just name -> t `pi` \ v -> substitute name v bodyType
-            _ -> t --> bodyType
-
-infixr `pi`
-
--- | Construct a pi type from a type and a function from an argument variable to the resulting type. The variable will be picked automatically. The parameter type will be checked against `Type`, as will the substitution of the parameter type into the body.
-pi :: Term Expression -> (Term Expression -> Term Expression) -> Term Expression
-pi t f = checkedExpression checkType $ Lambda t body
-  where body = abstract f
-        checkType expected context = case out expected of
-          Binding (Expression (Lambda from to)) -> checkTypeAgainst from to context
-          Type _ -> checkTypeAgainst _type' _type' context
-          _ -> checkTypeAgainst implicit implicit context >>= expectUnifiable expected
-        checkTypeAgainst from to context = do
-          _ <- checkIsType t context
-          _ <- expectUnifiable from t
-          bodyType <- checkIsType body (extendContext t context body)
-          _ <- expectUnifiable to bodyType
-          return $ case shadowing body bodyType of
-            Just name -> t `pi` \ v -> substitute name v bodyType
-            _ -> t --> bodyType
-
-infixr -->
-
--- | Construct a non-dependent function type between two types. Both operands will be checked against `Type`.
-(-->) :: Term Expression -> Term Expression -> Term Expression
-a --> b = checkedExpression (checkInferred inferType) $ Lambda a b
-  where inferType context = do
-          a' <- checkIsType a context
-          b' <- checkIsType b context
-          return $ a' --> b'
-
--- | Construct the application of one term to another. The first argument will be checked as a function type, and the second will be checked against that type’s domain. The resulting type will be the substitution of the domain type into the body.
-apply :: Term Expression -> Term Expression -> Term Expression
-apply a b = checkedExpression (checkInferred inferType) $ Application a b
-  where inferType context = do
-          (type', body) <- checkHasFunctionType a context
-          _ <- typeOf b type' context
-          return $ applySubstitution type' body
-
-
-checkHasFunctionType :: Term Expression -> Context (Term Expression) -> Result (Term Expression, Term Expression)
-checkHasFunctionType term context = inferTypeOf term context >>= checkIsFunctionType
-
-checkIsFunctionType :: Term Expression -> Result (Term Expression, Term Expression)
-checkIsFunctionType type' = case out type' of
-  Binding (Expression (Lambda type' body)) -> return (type', body)
-  _ -> Left "Expected function type."
-
-instance Monoid a => Alternative (Either a) where
-  empty = Left mempty
-  Left a <|> Left b = Left $ a `mappend` b
-  Right a <|> _ = Right a
-  _ <|> Right b = Right b
-
-checkIsType :: Term Expression -> Inferer (Term Expression)
-checkIsType term context = typeOf term _type' context <|> typeOf term (_type' --> _type') context
-
-
-instance Show (Term Expression) where
-  show = fst . para (\ b -> case b of
-    Binding (Variable n) -> (show n, maxBound)
-    Binding (Abstraction _ (_, body)) -> body
-
-    Type 0 -> ("Type", maxBound)
-    Type n -> ("Type" ++ showNumeral "₀₁₂₃₄₅₆₇₈₉" n, maxBound)
-
-    Binding (Expression (Application (_, a) (_, b))) -> (wrap 4 (<=) a ++ " " ++ wrap 4 (<) b, 4)
-
-    Binding (Expression (Lambda (_, type') (Term _ _ (Binding (Abstraction name term)), body))) | Set.member name (freeVariables term) -> ("λ " ++ show name ++ " : " ++ wrap 3 (<) type' ++ " . " ++ wrap 3 (<=) body, 3)
-    Binding (Expression (Lambda (_, type') (Term _ _ (Binding (Abstraction _ _)), body))) -> ("λ _ : " ++ wrap 3 (<) type' ++ " . " ++ wrap 3 (<=) body, 3)
-    Binding (Expression (Lambda (_, type') (_, body))) -> (wrap 3 (<) type' ++ " → " ++ wrap 3 (<=) body, 3)
-
-    Implicit -> ("_", maxBound)
-    Annotation (_, term) (_, type') -> (wrap 3 (<=) term ++ " : " ++ wrap 3 (<) type', 3)
-
-    :: (String, Int))
-    where wrap i op (s, j) | i `op` j = s
-          wrap _ _ (s, _) = "(" ++ s ++ ")"
+import Surface.Language as Surface'
+import Surface.Renaming as Surface'
+import Surface.Unification as Surface'