commit f844d389f0a9897b15b65d8a07a2f2dd7bc9195d
parent 425f792ed11130eb72952ebae0dd631e13b29e61
Author: Robert Russell <robert@rr3.xyz>
Date: Sat, 23 May 2026 14:41:12 -0700
Add phantom parameter to Depth, Index, Level, and Environment
Diffstat:
2 files changed, 25 insertions(+), 19 deletions(-)
diff --git a/src/PlUtils/DeBruijn.hs b/src/PlUtils/DeBruijn.hs
@@ -19,35 +19,41 @@ import PlUtils.Util
-- Indices and levels
-- | A @Nat@ representing the number of free variables in some context.
-newtype Depth = Depth {unDepth :: Nat} deriving (Show, Eq)
+--
+-- The @syn@ phantom type parameter separates depths for different environments.
+newtype Depth syn = Depth {unDepth :: Nat} deriving (Show, Eq)
-- | A de Bruijn index represented as a @Nat@, that is, an index into a context
-- "from the right", such that the innermost free variable gets index 0.
-newtype Index = Index {unIndex :: Nat} deriving (Show, Eq)
+--
+-- The @syn@ phantom type parameter separates indices for different syntaxes.
+newtype Index syn = Index {unIndex :: Nat} deriving (Show, Eq)
-- | A de Bruijn level represented as a @Nat@, that is, an index into a context
-- "from the left", such that the outermost free variable gets index 0.
-newtype Level = Level {unLevel :: Nat} deriving (Show, Eq)
+--
+-- The @syn@ phantom type parameter separates levels for different syntaxes.
+newtype Level syn = Level {unLevel :: Nat} deriving (Show, Eq)
-descend :: Depth -> (Level, Depth)
+descend :: Depth syn -> (Level syn, Depth syn)
descend (Depth d) = assert (d < maxBound) "PlUtils: depth overflow" (Level d, Depth (d + 1))
-idxInBounds :: Depth -> Index -> Bool
+idxInBounds :: Depth syn -> Index syn -> Bool
idxInBounds (Depth d) (Index i) = i < d
-lvlInBounds :: Depth -> Level -> Bool
+lvlInBounds :: Depth syn -> Level syn -> Bool
lvlInBounds (Depth d) (Level l) = l < d
-assertIdxInBounds :: Depth -> Index -> a -> a
+assertIdxInBounds :: Depth syn -> Index syn -> a -> a
assertIdxInBounds d i = assert (idxInBounds d i) "PlUtils: index out of bounds"
-assertLvlInBounds :: Depth -> Level -> a -> a
+assertLvlInBounds :: Depth syn -> Level syn -> a -> a
assertLvlInBounds d l = assert (lvlInBounds d l) "PlUtils: level out of bounds"
-idxToLvl :: Depth -> Index -> Level
+idxToLvl :: Depth syn -> Index syn -> Level syn
idxToLvl d i = assertIdxInBounds d i $ Level (unDepth d - unIndex i - 1)
-lvlToIdx :: Depth -> Level -> Index
+lvlToIdx :: Depth syn -> Level syn -> Index syn
lvlToIdx d l = assertLvlInBounds d l $ Index (unDepth d - unLevel l - 1)
--------------------------------------------------------------------------------
diff --git a/src/PlUtils/Environment.hs b/src/PlUtils/Environment.hs
@@ -21,33 +21,33 @@ import PlUtils.DeBruijn
-- stable under weakening, so we don't need to modify the environment when
-- descending under a binder) and with syntactic variables represented as
-- de Bruijn indices.
-data Environment v = Environment Depth (NatMap v) deriving (Show)
+data Environment syn v = Environment (Depth syn) (NatMap v) deriving (Show)
-empty :: Environment v
+empty :: Environment syn v
empty = Environment (Depth 0) NatMap.empty
-depth :: Environment v -> Depth
+depth :: Environment syn v -> Depth syn
depth (Environment d _) = d
-- | Bind a new variable (without introducing a substitution for it).
-bind :: Environment v -> (Level, Environment v)
+bind :: Environment syn v -> (Level syn, Environment syn v)
bind (Environment d s) =
let (l, d') = descend d
in (l, Environment d' s)
-weaken :: Environment v -> Environment v
+weaken :: Environment syn v -> Environment syn v
weaken = snd . bind
-- | Assign a value to an existing variable.
-assign :: Level -> v -> Environment v -> Environment v
+assign :: Level syn -> v -> Environment syn v -> Environment syn v
assign l v (Environment d s) = assertLvlInBounds d l $ Environment d (NatMap.insert (unLevel l) v s)
-- | Lookup the substitution for a variable.
-lookup :: Level -> Environment v -> Maybe v
+lookup :: Level syn -> Environment syn v -> Maybe v
lookup l (Environment d s) = assertLvlInBounds d l $ NatMap.lookup (unLevel l) s
-- | Bind and a new variable and assign a value to it.
-define :: (Level -> v) -> Environment v -> Environment v
+define :: (Level syn -> v) -> Environment syn v -> Environment syn v
define makeVal env =
let (l, env') = bind env
in assign l (makeVal l) env'
@@ -55,7 +55,7 @@ define makeVal env =
-- | Evaluate an index in an environment, falling back to making a value with
-- the given function in case the environment doesn't have a substitution for
-- the index.
-eval :: (Level -> v) -> Index -> Environment v -> v
+eval :: (Level syn -> v) -> Index syn -> Environment syn v -> v
eval makeVal i env =
let l = idxToLvl (depth env) i
in fromMaybe (makeVal l) $ lookup l env
