Initial commit

Author: LightAndLight

.gitignore

@@ -0,0 +1,3 @@
+dist/
+dist-newstyle/
+.ghc.*

CHANGELOG.md

@@ -0,0 +1,5 @@
+# Revision history for qtt
+
+## 0.1.0.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.

LICENSE

@@ -0,0 +1,30 @@
+Copyright (c) 2019, Isaac Elliott
+
+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 Isaac Elliott 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.

Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain

qtt.cabal

@@ -0,0 +1,27 @@
+cabal-version:       2.4
+-- Initial package description 'qtt.cabal' generated by 'cabal init'.  For
+-- further documentation, see http://haskell.org/cabal/users-guide/
+
+name:                qtt
+version:             0.1.0.0
+-- synopsis:
+-- description:
+-- bug-reports:
+license:             BSD-3-Clause
+license-file:        LICENSE
+author:              Isaac Elliott
+maintainer:          [email protected]
+-- copyright:
+category:            Language
+extra-source-files:  CHANGELOG.md
+
+library
+  exposed-modules:     Syntax
+                     , Context
+  build-depends:       base ^>=4.12.0.0
+                     , bound
+                     , deriving-compat
+                     , semirings
+  ghc-options:         -Wall -Werror
+  hs-source-dirs:      src
+  default-language:    Haskell2010

src/Context.hs

@@ -0,0 +1,42 @@
+{-# language DeriveFunctor #-}
+module Context where
+
+import Data.Semiring (times, plus)
+import Syntax
+
+data Entry v a
+  = Entry
+  { _entryVar :: v
+  , _entryUsage :: Usage
+  , _entryType :: Term a
+  } deriving (Eq, Show, Functor)
+
+newtype Context a = Context { unContext :: [Entry a a] }
+  deriving (Eq, Show)
+
+scaleC :: Usage -> Context a -> Context a
+scaleC u = Context . go . unContext
+  where
+    go ctx =
+      case ctx of
+        [] -> []
+        Entry v u' t : cs -> Entry v (times u u') t : go cs
+
+zeroC :: Context a -> Context a
+zeroC = scaleC Zero
+
+addC :: Eq a => Context a -> Context a -> Context a
+addC (Context a) (Context b) = Context $ go a b
+  where
+    go [] [] = []
+    go (Entry v u t : cs) (Entry v' u' t' : cs')
+      | v == v' && t == t' = Entry v (plus u u') t : go cs cs'
+    go _ _ =  error "addContext: context mismatch"
+
+lookupC :: Eq a => a -> Context a -> Maybe (Entry a a)
+lookupC a = go . unContext
+  where
+    go [] = Nothing
+    go (Entry v u t : cs)
+      | v == a = Just $ Entry v u t
+      | otherwise = go cs

src/Syntax.hs

@@ -0,0 +1,49 @@
+{-# language DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
+{-# language StandaloneDeriving #-}
+{-# language TemplateHaskell #-}
+module Syntax where
+
+import Bound.Scope (Scope)
+import Bound.TH (makeBound)
+import Data.Deriving (deriveEq1, deriveShow1)
+
+import Data.Semiring (Semiring(..))
+
+data Usage = Zero | One | Many
+  deriving (Eq, Show)
+
+instance Semiring Usage where
+  zero = Zero
+  one = One
+
+  plus Zero m = m
+  plus One Zero = One
+  plus One One = Many
+  plus One Many = Many
+  plus Many m = Many
+
+  times Zero m = Zero
+  times One m = m
+  times Many Zero = Zero
+  times Many One = Many
+  times Many Many = Many
+
+type Ty = Term
+data Term a
+  = Var a
+  | Ann (Term a) Usage (Term a)
+  | Type
+  | Lam (Scope () Term a)
+  | Pi Usage (Term a) (Scope () Term a)
+  | App (Term a) (Term a)
+  | Pair (Term a) (Term a)
+  | Sigma Usage (Term a) (Scope () Term a)
+  | Fst (Term a)
+  | Snd (Term a)
+  deriving (Functor, Foldable, Traversable)
+makeBound ''Term
+deriveEq1 ''Term
+deriveShow1 ''Term
+
+deriving instance Eq a => Eq (Term a)
+deriving instance Show a => Show (Term a)

src/Typecheck.hs

@@ -0,0 +1,52 @@
+module Typecheck where
+
+import Bound.Scope (fromScope)
+import Bound.Var (Var(..), unvar)
+
+import Context
+import Syntax
+
+data TypeError a
+  = NotInScope a
+  | VariableMany a
+  | ExpectedType (Ty a)
+  deriving (Eq, Show)
+
+eval :: Context a -> Term a -> Term a
+eval ctx tm =
+  case tm of
+    Var a -> _
+    Ann a u b -> _
+    Type -> Type
+    Lam a -> _
+    Pi u a b -> _
+    App a b -> _
+    Pair a b -> _
+    Sigma u a b -> _
+    Fst a -> _
+    Snd a -> _
+
+check :: Context a -> (x -> Entry () x) -> Term x -> Usage -> Ty x -> Either (TypeError a) Bool
+check ctx varCtx tm u ty =
+  case tm of
+    Pi u a b ->
+      case ty of
+        Type -> do
+          check (zeroC ctx) varCtx a Zero Type
+          check (zeroC ctx) (unvar (const $ Entry () Zero (F <$> a)) (fmap F . varCtx)) (fromScope b) Zero Type
+        _ -> Left $ ExpectedType ty
+
+infer :: Eq a => Context a -> Term a -> Either (TypeError a) (Usage, Ty a)
+infer ctx tm =
+  case tm of
+    Var a ->
+      case lookupC a ctx of
+        Nothing -> Left $ NotInScope a
+        Just (Entry _ u t) ->
+          case u of
+            Many -> Left $ VariableMany a
+            _ -> pure (u, t)
+    Ann a u b -> do
+      check (zeroC ctx) b Zero Type
+      check (zeroC ctx) a Zero b
+      pure (u, b)