commit 0ea9e9063f42a26bf96de209911415392f3375c6
parent 4ccc8ed82ddcf5de69f0d2aaeb572b8a01f3b9e4
Author: Robert Russell <robert@rr3.xyz>
Date: Tue, 27 Aug 2024 18:58:30 -0700
Elaborate types
Diffstat:
| A | Core.hs | | | 37 | +++++++++++++++++++++++++++++++++++++ |
| A | Main.hs | | | 123 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| A | Surface.hs | | | 41 | +++++++++++++++++++++++++++++++++++++++++ |
| A | package.yaml | | | 42 | ++++++++++++++++++++++++++++++++++++++++++ |
| A | stack.yaml | | | 5 | +++++ |
5 files changed, 248 insertions(+), 0 deletions(-)
diff --git a/Core.hs b/Core.hs
@@ -0,0 +1,37 @@
+module Core where
+import qualified Surface as S
+
+newtype TypeIndex = TypeIndex Int deriving Show
+newtype TermIndex = TermIndex Int deriving Show
+
+type Kind = S.Kind
+
+data Type q
+ = TypeVar TypeIndex
+
+ | TypeTArrow (Type q) (Type q)
+ | TypeTForall Kind (Type q)
+
+ | TypeQ q
+ -- TODO: Internal Mul and Add operations?
+
+ | TypeQTPair (Type q) (Type q)
+ | TypeQTFst (Type q)
+ | TypeQTSnd (Type q)
+
+ | TypeArrowAbs (Type q)
+ | TypeArrowApp (Type q) (Type q)
+ deriving Show
+
+data Term q
+ = TermVar TermIndex
+
+ | TermArrowAbs (Term q)
+ | TermArrowApp (Term q) (Term q)
+
+ | TermForallAbs (Term q)
+ | TermForallApp (Term q) (Type q)
+ deriving Show
+
+newtype TypeLevel = TypeLevel Int deriving Show
+newtype TermLevel = TermLevel Int deriving Show
diff --git a/Main.hs b/Main.hs
@@ -0,0 +1,123 @@
+module Main where
+import Control.Monad
+import Control.Monad.Except
+import Control.Monad.Reader
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
+import Safe (atMay)
+
+import Algebra
+import Ledger (Ledger)
+import qualified Ledger as L
+import Surface (Kind (..))
+import qualified Surface as S
+import qualified Core as C
+
+--------------------------------------------------------------------------------
+-- Util
+
+orThrowError :: MonadError e m => Maybe a -> e -> m a
+a `orThrowError` e =
+ case a of
+ Just x -> return x
+ Nothing -> throwError e
+
+mapInsertCons :: Ord k => k -> v -> Map k [v] -> Map k [v]
+mapInsertCons k v =
+ let f (Just vs) = Just (v : vs)
+ f Nothing = Just [v]
+ in Map.alter f k
+
+--------------------------------------------------------------------------------
+-- Context
+-- TODO: move to separate module
+
+data Ctx q = Ctx {
+ nTypes :: Int,
+ types :: Map S.TypeName [(C.TypeLevel, Kind)],
+ nTerms :: Int,
+ terms :: Map S.TermName [(C.TermLevel, C.Type q)]
+}
+
+ctxEmpty :: Ctx q
+ctxEmpty = Ctx 0 Map.empty 0 Map.empty
+
+ctxBindType :: S.TypeName -> Kind -> Ctx q -> Ctx q
+ctxBindType x k ctx =
+ let lvl = C.TypeLevel ctx.nTypes in
+ ctx {
+ nTypes = ctx.nTypes + 1,
+ types = mapInsertCons x (lvl, k) ctx.types
+ }
+
+ctxLookupType :: S.TypeName -> Ctx q -> Maybe (C.TypeLevel, Kind)
+ctxLookupType x ctx = do
+ xBindings <- Map.lookup x ctx.types
+ xBindings `atMay` 0
+
+ctxTypeLevelToIndex :: C.TypeLevel -> Ctx q -> C.TypeIndex
+ctxTypeLevelToIndex (C.TypeLevel lvl) ctx = C.TypeIndex (ctx.nTypes - lvl - 1)
+
+--------------------------------------------------------------------------------
+-- Elaboration
+
+data Err = Err
+
+type Elab q a = ReaderT (Ctx q) (Except Err) a
+
+bindType :: S.TypeName -> Kind -> Elab q a -> Elab q a
+bindType x k = local (ctxBindType x k)
+
+lookupType :: S.TypeName -> Elab q (C.TypeLevel, Kind)
+lookupType x = asks (ctxLookupType x) >>= (`orThrowError` Err) -- TODO
+
+typeLevelToIndex :: C.TypeLevel -> Elab q C.TypeIndex
+typeLevelToIndex lvl = asks (ctxTypeLevelToIndex lvl)
+
+inferType :: S.Type q -> Elab q (C.Type q, Kind)
+inferType = \case
+ S.TypeVar x -> do
+ (lvl, k) <- lookupType x
+ idx <- typeLevelToIndex lvl
+ pure (C.TypeVar idx, k)
+ S.TypeAnnot a k -> (, k) <$> checkType a k
+ S.TypeTArrow dom cod -> do
+ dom' <- checkType dom KindQT
+ cod' <- checkType cod KindQT
+ pure (C.TypeTArrow dom' cod', KindT)
+ S.TypeTForall x k a -> do
+ a' <- bindType x k $ checkType a KindQT
+ pure (C.TypeTForall k a', KindT)
+ S.TypeQ q -> pure (C.TypeQ q, KindQ)
+ S.TypeQTPair q a -> do
+ q' <- checkType q KindQ
+ a' <- checkType a KindT
+ pure (C.TypeQTPair q' a', KindQT)
+ S.TypeQTFst qa -> do
+ qa' <- checkType qa KindQT
+ pure (C.TypeQTFst qa', KindQ)
+ S.TypeQTSnd qa -> do
+ qa' <- checkType qa KindQT
+ pure (C.TypeQTSnd qa', KindT)
+ S.TypeArrowAbs _ _ -> throwError Err -- TODO
+ S.TypeArrowApp fun arg -> do
+ (fun', k) <- inferType fun
+ case k of
+ KindArrow dom cod -> do
+ arg' <- checkType arg dom
+ pure (C.TypeArrowApp fun' arg', cod)
+ _ -> throwError Err -- TODO
+
+checkType :: S.Type q -> Kind -> Elab q (C.Type q)
+checkType a k = case (a, k) of
+ (S.TypeArrowAbs x body, KindArrow dom cod) ->
+ bindType x dom $ checkType body cod
+ (a, k) -> do
+ (a', k') <- inferType a
+ unless (k' == k) $ throwError Err -- TODO
+ pure a'
+
+--------------------------------------------------------------------------------
+
+main :: IO ()
+main = putStrLn "whoa"
diff --git a/Surface.hs b/Surface.hs
@@ -0,0 +1,41 @@
+module Surface where
+import Data.ByteString (ByteString)
+
+newtype TypeName = TypeName ByteString deriving (Eq, Ord, Show)
+newtype TermName = TermName ByteString deriving (Eq, Ord, Show)
+
+data Kind
+ = KindT
+ | KindQ
+ | KindQT
+ | KindArrow Kind Kind
+ deriving (Eq, Show)
+
+data Type q
+ = TypeVar TypeName
+ | TypeAnnot (Type q) Kind
+
+ | TypeTArrow (Type q) (Type q)
+ | TypeTForall TypeName Kind (Type q)
+
+ | TypeQ q
+ -- TODO: Internal Mul and Add operations?
+
+ | TypeQTPair (Type q) (Type q)
+ | TypeQTFst (Type q)
+ | TypeQTSnd (Type q)
+
+ | TypeArrowAbs TypeName (Type q)
+ | TypeArrowApp (Type q) (Type q)
+ deriving Show
+
+data Term q
+ = TermVar TermName
+ | TermAnnot (Term q) (Type q)
+
+ | TermArrowAbs TermName (Term q)
+ | TermArrowApp (Term q) (Term q)
+
+ | TermForallAbs TypeName (Term q)
+ | TermForallApp (Term q) (Type q)
+ deriving Show
diff --git a/package.yaml b/package.yaml
@@ -0,0 +1,42 @@
+name: systemqfw
+version: 0.1.0.0
+author: "Robert Russell"
+license: ISC
+
+ghc-options:
+ - -Wall
+ - -Wno-name-shadowing
+ - -Wno-missing-signatures
+
+default-extensions:
+ - DuplicateRecordFields
+ - NoFieldSelectors
+ - OverloadedRecordDot
+
+ - BlockArguments
+ - LambdaCase
+ - MultiWayIf
+ - TupleSections
+ - OverloadedStrings
+
+ - ScopedTypeVariables
+ - TypeFamilies
+ - FlexibleContexts
+ - TypeOperators
+
+ - FlexibleInstances
+ - MultiParamTypeClasses
+ - UndecidableInstances
+
+dependencies:
+ - base >= 4.18 && < 5
+ - bytestring
+ - containers
+ - mtl
+ - safe
+ - sparsec
+
+executables:
+ systemqfw:
+ source-dirs: .
+ main: Main.hs
diff --git a/stack.yaml b/stack.yaml
@@ -0,0 +1,5 @@
+resolver: lts-22.23
+
+packages:
+ - .
+ - sparsec
