commit 4cab45d1225520984f81a0602d66087e1eec8667
parent 7f3dfd2b1726b292156a06623c97d2ebdccb04c1
Author: Robert Russell <robert@rr3.xyz>
Date: Tue, 27 Aug 2024 22:41:09 -0700
Work out abstraction for contexts/environments
This could be useful in a toy-PL-development library...
Diffstat:
| A | Context.hs | | | 106 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| M | Core.hs | | | 12 | ++++++------ |
| A | Environment.hs | | | 42 | ++++++++++++++++++++++++++++++++++++++++++ |
| M | Ledger.hs | | | 22 | ++++++++++++---------- |
| M | Main.hs | | | 107 | +++++++++++++++++++++++++++++++++++++++++-------------------------------------- |
| M | Surface.hs | | | 1 | + |
| A | Util.hs | | | 9 | +++++++++ |
| A | Value.hs | | | 72 | ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| M | package.yaml | | | 2 | ++ |
9 files changed, 306 insertions(+), 67 deletions(-)
diff --git a/Context.hs b/Context.hs
@@ -0,0 +1,106 @@
+module Context where
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
+import Safe (atMay)
+
+import Util
+import Environment (Env)
+import qualified Environment as Env
+
+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
+
+class Value a where
+ type Generic a
+ generic :: Generic a -> a
+
+type Ctx' name idx lvl a b =
+ (Ord name, IsInt idx, IsInt lvl, Value a, Generic a ~ lvl)
+data Ctx name idx lvl a b = Ctx {
+ map :: Map name [(a, b)],
+ env :: Env idx lvl a
+}
+
+empty :: Ctx' name idx lvl a b
+ => Ctx name idx lvl a b
+empty = Ctx Map.empty Env.empty
+
+assign :: Ctx' name idx lvl a b
+ => name -> a -> b -> Ctx name idx lvl a b -> Ctx name idx lvl a b
+assign x a b ctx = ctx { map = mapInsertCons x (a, b) ctx.map }
+
+lookup :: Ctx' name idx lvl a b
+ => name -> Int -> Ctx name idx lvl a b -> Maybe (a, b)
+lookup x i ctx = do
+ xAsns <- Map.lookup x ctx.map
+ xAsns `atMay` i
+
+bind :: Ctx' name idx lvl a b
+ => Ctx name idx lvl a b -> (lvl, Ctx name idx lvl a b)
+bind ctx =
+ let (l, env') = Env.bind ctx.env
+ in (l, ctx { env = env' })
+
+bindAndAssign :: Ctx' name idx lvl a b
+ => name -> b -> Ctx name idx lvl a b -> (lvl, Ctx name idx lvl a b)
+bindAndAssign x b ctx =
+ let (l, ctx') = bind ctx
+ in (l, assign x (generic l) b ctx')
+
+idxToLvl :: Ctx' name idx lvl a b
+ => idx -> Ctx name idx lvl a b -> lvl
+idxToLvl i ctx = Env.idxToLvl i ctx.env
+
+lvlToIdx :: Ctx' name idx lvl a b
+ => lvl -> Ctx name idx lvl a b -> idx
+lvlToIdx l ctx = Env.lvlToIdx l ctx.env
+
+define :: Ctx' name idx lvl a b
+ => lvl -> a -> Ctx name idx lvl a b -> Ctx name idx lvl a b
+define l a ctx = ctx { env = Env.define l a ctx.env }
+
+eval :: Ctx' name idx lvl a b
+ => lvl -> Ctx name idx lvl a b -> Maybe a
+eval l ctx = Env.eval l ctx.env
+
+{-
+data Ctx q = Ctx (TypeCtx q) (TermCtx 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)
+
+ctxBindTerm :: S.TermName -> V.Type q -> Ctx q -> Ctx q
+ctxBindTerm x a ctx =
+ let lvl = C.TermLevel ctx.nTerms in
+ ctx {
+ nTerms = ctx.nTerms + 1,
+ terms = mapInsertCons x (lvl, a) ctx.terms
+ }
+
+ctxLookupTerm :: S.TermName -> Ctx q -> Maybe (C.TermLevel, V.Type q)
+ctxLookupTerm x ctx = do
+ xBindings <- Map.lookup x ctx.terms
+ xBindings `atMay` 0
+
+ctxTermLevelToIndex :: C.TermLevel -> Ctx q -> C.TermIndex
+ctxTermLevelToIndex (C.TermLevel lvl) ctx = C.TermIndex (ctx.nTerms - lvl - 1)
+-}
diff --git a/Core.hs b/Core.hs
@@ -1,8 +1,10 @@
module Core where
+
+import Util
import qualified Surface as S
-newtype TypeIndex = TypeIndex Int deriving Show
-newtype TermIndex = TermIndex Int deriving Show
+newtype TypeIndex = TypeIndex Int deriving (Show, IsInt)
+newtype TermIndex = TermIndex Int deriving (Show, IsInt)
type Kind = S.Kind
@@ -13,7 +15,8 @@ data Type q
| TypeTForall Kind (Type q)
| TypeQ q
- -- TODO: Internal Mul and Add operations?
+ | TypeQAdd (Type q) (Type q)
+ | TypeQMul (Type q) (Type q)
| TypeQTPair (Type q) (Type q)
| TypeQTFst (Type q)
@@ -32,6 +35,3 @@ data 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/Environment.hs b/Environment.hs
@@ -0,0 +1,42 @@
+module Environment where
+import Data.IntMap.Strict (IntMap)
+import qualified Data.IntMap.Strict as IntMap
+
+import Util
+
+type Env' idx lvl = (IsInt idx, IsInt lvl)
+data Env idx lvl a = Env Int (IntMap a)
+
+empty :: Env' idx lvl => Env idx lvl a
+empty = Env 0 IntMap.empty
+
+bind :: Env' idx lvl => Env idx lvl a -> (lvl, Env idx lvl a)
+bind (Env size map) = (fromInt size, Env (size + 1) map)
+
+idxToLvl :: Env' idx lvl => idx -> Env idx lvl a -> lvl
+idxToLvl i (Env size _) =
+ if toInt i >= size then
+ error "Env.idxToLvl: index out of range"
+ else
+ fromInt $ size - toInt i - 1
+
+lvlToIdx :: Env' idx lvl => lvl -> Env idx lvl a -> idx
+lvlToIdx l (Env size _) =
+ if toInt l >= size then
+ error "Env.lvlToIdx: level out of range"
+ else
+ fromInt $ size - toInt l - 1
+
+define :: Env' idx lvl => lvl -> a -> Env idx lvl a -> Env idx lvl a
+define l v (Env size map) =
+ if toInt l >= size then
+ error "Env.define: level out of range"
+ else
+ Env size (IntMap.insert (toInt l) v map)
+
+eval :: Env' idx lvl => lvl -> Env idx lvl a -> Maybe a
+eval l (Env size map) =
+ if toInt l >= size then
+ error "Env.eval: level out of range"
+ else
+ IntMap.lookup (toInt l) map
diff --git a/Ledger.hs b/Ledger.hs
@@ -3,18 +3,20 @@ import Data.IntMap.Strict (IntMap)
import qualified Data.IntMap.Strict as IntMap
import Algebra
-import qualified Core as C
+import qualified Value as V
--- A ledger maps from de Bruijn levels (represented as Ints) to quantities
--- (represented as some type q). This mapping is implemented with an IntMap
--- and a default quantity for all variable not in the IntMap.
-data Ledger q = Ledger q (IntMap q)
+-- A ledger maps from de Bruijn levels (represented as Ints) to quantities.
+-- This mapping is implemented with an IntMap and a default quantity for all
+-- variables not in the IntMap.
+data Ledger q = Ledger (V.Type q) (IntMap (V.Type q))
+{-
-- Pointwise LUB
instance LubMonoid q => LubMonoid (Ledger q) where
bot = Ledger bot IntMap.empty
Ledger d0 m0 <^> Ledger d1 m1 = Ledger (d0 <^> d1) (IntMap.unionWith (<^>) m0 m1)
+-}
-- Pointwise sum
instance AddMonoid q => AddMonoid (Ledger q) where
@@ -24,16 +26,16 @@ instance AddMonoid q => AddMonoid (Ledger q) where
-- Scalar multiply mapped over the entire ledger
instance (MulAction q, MulActionScalar q ~ q) => MulAction (Ledger q) where
- type MulActionScalar (Ledger q) = q
+ type MulActionScalar (Ledger q) = V.Type q
q <⋅> Ledger d m = Ledger (q <⋅> d) ((q <⋅>) <$> m)
-singleton :: AddMonoid q => C.TermLevel -> q -> Ledger q
-singleton (C.TermLevel l) q = Ledger zero (IntMap.singleton l q)
+singleton :: AddMonoid q => V.TermLevel -> V.Type q -> Ledger q
+singleton (V.TermLevel l) q = Ledger zero (IntMap.singleton l q)
-- split is like uncons for ledgers: given a ledger L that maps a de Bruijn
-- level l to quantity q, "split l L" returns (q, L'), where L' is L with the
-- mapping for l removed (i.e., l is reset to the default quantity).
-split :: C.TermLevel -> Ledger q -> (q, Ledger q)
-split (C.TermLevel l) (Ledger d m) =
+split :: V.TermLevel -> Ledger q -> (V.Type q, Ledger q)
+split (V.TermLevel l) (Ledger d m) =
(IntMap.findWithDefault d l m, Ledger d (IntMap.delete l m))
diff --git a/Main.hs b/Main.hs
@@ -2,16 +2,17 @@ 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 Data.Functor
import Algebra
import Ledger (Ledger)
import qualified Ledger as L
+import Context (Ctx)
+import qualified Context as Ctx
import Surface (Kind (..))
import qualified Surface as S
import qualified Core as C
+import qualified Value as V
--------------------------------------------------------------------------------
-- Util
@@ -22,71 +23,49 @@ a `orThrowError` e =
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 monad
---------------------------------------------------------------------------------
--- Elaboration
+type TypeCtx q = Ctx S.TypeName C.TypeIndex V.TypeLevel (V.Type q) Kind
+
+type TermCtx q = Ctx S.TermName C.TermIndex V.TermLevel V.Term (V.Type q)
data Err = Err
-type Elab q a = ReaderT (Ctx q) (Except Err) a
+type Elab q a = ReaderT (TypeCtx q, TermCtx q) (Except Err) a
+
+askTypeCtx :: Elab q (TypeCtx q)
+askTypeCtx = asks fst
-bindType :: S.TypeName -> Kind -> Elab q a -> Elab q a
-bindType x k = local (ctxBindType x k)
+askTermCtx :: Elab q (TermCtx q)
+askTermCtx = asks snd
-lookupType :: S.TypeName -> Elab q (C.TypeLevel, Kind)
-lookupType x = asks (ctxLookupType x) >>= (`orThrowError` Err) -- TODO
+--------------------------------------------------------------------------------
+-- Type-level elaboration
+
+bindAndAssignType :: S.TypeName -> Kind -> Elab q a -> Elab q a
+bindAndAssignType x k = local \(typeCtx, termCtx) ->
+ (snd $ Ctx.bindAndAssign x k typeCtx, termCtx)
-typeLevelToIndex :: C.TypeLevel -> Elab q C.TypeIndex
-typeLevelToIndex lvl = asks (ctxTypeLevelToIndex lvl)
+lookupType :: S.TypeName -> Elab q (V.Type q, Kind)
+lookupType x = (Ctx.lookup x 0 <$> askTypeCtx) >>= (`orThrowError` Err) -- TODO
+
+typeLvlToIdx :: V.TypeLevel -> Elab q C.TypeIndex
+typeLvlToIdx lvl = Ctx.lvlToIdx lvl <$> askTypeCtx
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)
+ (va, k) <- lookupType x
+ typeEnv <- askTypeCtx <&> (.env)
+ pure (V.quote typeEnv va, 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
+ a' <- bindAndAssignType x k $ checkType a KindQT
pure (C.TypeTForall k a', KindT)
S.TypeQ q -> pure (C.TypeQ q, KindQ)
S.TypeQTPair q a -> do
@@ -111,13 +90,39 @@ inferType = \case
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
+ bindAndAssignType x dom $ checkType body cod
(a, k) -> do
(a', k') <- inferType a
unless (k' == k) $ throwError Err -- TODO
pure a'
--------------------------------------------------------------------------------
+-- Term-level elaboration
+
+{-
+bindTerm :: S.TermName -> V.Type q -> Elab q a -> Elab q a
+bindTerm x a = local (ctxBindTerm x a)
+
+lookupTerm :: S.TermName -> Elab q (C.TermLevel, V.Type q)
+lookupTerm x = asks (ctxLookupTerm x) >>= (`orThrowError` Err) -- TODO
+
+termLevelToIndex :: C.TermLevel -> Elab q C.TermIndex
+termLevelToIndex lvl = asks (ctxTermLevelToIndex lvl)
+
+inferTerm :: S.Term q -> V.Term q -> Elab q (C.Term q, V.Type q, Ledger q)
+inferTerm t q = case t of
+ S.TermVar x -> do
+ (lvl, a) <- lookupTerm x
+ idx <- termLevelToIndex lvl
+ pure (C.TermVar idx, a, Ledger.singleton lvl q)
+ S.TermAnnot t a -> do
+ a' <- checkType a KindT
+
+checkTerm :: S.Term q -> V.Type q -> V.Type q -> Elab q (C.Term q, Ledger q)
+checkTerm t a =
+-}
+
+--------------------------------------------------------------------------------
main :: IO ()
main = putStrLn "whoa"
diff --git a/Surface.hs b/Surface.hs
@@ -4,6 +4,7 @@ import Data.ByteString (ByteString)
newtype TypeName = TypeName ByteString deriving (Eq, Ord, Show)
newtype TermName = TermName ByteString deriving (Eq, Ord, Show)
+-- TODO: Move this?
data Kind
= KindT
| KindQ
diff --git a/Util.hs b/Util.hs
@@ -0,0 +1,9 @@
+module Util where
+
+class IsInt a where
+ toInt :: a -> Int
+ fromInt :: Int -> a
+
+instance IsInt Int where
+ toInt = id
+ fromInt = id
diff --git a/Value.hs b/Value.hs
@@ -0,0 +1,72 @@
+module Value where
+
+import Util
+import Algebra
+import Environment (Env)
+import qualified Environment as Env
+import qualified Context as Ctx
+import Surface (Kind (..))
+import qualified Core as C
+
+newtype TypeLevel = TypeLevel Int deriving (Show, IsInt)
+newtype TermLevel = TermLevel Int deriving (Show, IsInt)
+
+type TypeEnv q = Env C.TypeIndex TypeLevel (Type q)
+data TypeClosure q = TypeClosure (TypeEnv q) (C.Type q)
+
+data TypeElim q
+ = TypeElimFst
+ | TypeElimSnd
+ | TypeElimApp (Type q)
+ | TypeElimAdd (Type q)
+ | TypeElimMul (Type q)
+
+data Type q
+ = TypeNeutral TypeLevel [TypeElim q]
+
+ | TypeTArrow (Type q) (Type q)
+ | TypeTForall Kind (TypeClosure q)
+
+ | TypeQ q
+
+ | TypeQTPair (Type q) (Type q)
+
+ | TypeArrowAbs (TypeClosure q)
+
+instance Ctx.Value (Type q) where
+ type Generic (Type q) = TypeLevel
+ generic l = TypeNeutral l []
+
+instance AddMonoid q => AddMonoid (Type q) where
+ zero = TypeQ zero
+
+ a <+> b = case (a, b) of
+ (TypeQ q, TypeQ r) -> TypeQ (q <+> r)
+ (TypeNeutral l es, a) -> TypeNeutral l (TypeElimAdd a : es)
+ (a, TypeNeutral l es) -> TypeNeutral l (TypeElimAdd a : es)
+ _ -> error "impossible"
+
+instance MulScalar q => MulScalar (Type q) where
+ one = TypeQ one
+
+instance (MulAction q, MulActionScalar q ~ q) => MulAction (Type q) where
+ type MulActionScalar (Type q) = Type q
+
+ a <⋅> b = case (a, b) of
+ (TypeQ q, TypeQ r) -> TypeQ (q <⋅> r)
+ (TypeNeutral l es, a) -> TypeNeutral l (TypeElimMul a : es)
+ (a, TypeNeutral l es) -> TypeNeutral l (TypeElimMul a : es)
+ _ -> error "impossible"
+
+-- During elaboration, we only need to "evaluate" term variables.
+data Term = TermGeneric TermLevel
+
+instance Ctx.Value Term where
+ type Generic Term = TermLevel
+ generic = TermGeneric
+
+eval :: TypeEnv q -> C.Type q -> Type q
+eval = eval
+
+quote :: TypeEnv q -> Type q -> C.Type q
+quote = quote
diff --git a/package.yaml b/package.yaml
@@ -23,10 +23,12 @@ default-extensions:
- TypeFamilies
- FlexibleContexts
- TypeOperators
+ - ConstraintKinds
- FlexibleInstances
- MultiParamTypeClasses
- UndecidableInstances
+ - GeneralizedNewtypeDeriving
dependencies:
- base >= 4.18 && < 5
