haskell: + Administrative normal form

https://en.wikipedia.org/wiki/A-normal_form
https://matt.might.net/articles/a-normalization/

but see also:
- KNF: https://esumii.github.io/min-caml/tutorial-mincaml-9.eng.htm

haskell/nfker7h/lib/Language/Yanais/Nfker7h/Anf.hs

@@ -0,0 +1,127 @@
+{-# LANGUAGE DeriveGeneric #-}
+
+-- | Administrative normal form
+module Language.Yanais.Nfker7h.Anf (
+    AtomicExpr(..),
+    PatternInf(..),
+    Expr(..),
+    patAllocSlots,
+
+    NeutralRoot(..),
+    EvalError(..),
+    Value(..),
+    eval,
+) where
+
+import Control.Monad.Reader (ReaderT(..), MonadReader(..), asks, runReaderT)
+import Data.Hashable (Hashable)
+import Generic.Data (Generic)
+import Numeric.Natural
+
+-- import Language.Yanais.Parser.Lex (Ident, nullIdent)
+import Language.Yanais.Nfker7h.Literal
+
+data AtomicExpr = AELiteral Literal
+  | AEBound Natural
+  -- a lambda always takes up a single stack slot,
+  -- potentially necessary binder pattern matching happens in embedded let bindings
+  | AELambda Expr
+  -- a pi is similar to a lambda, but the binder type is also present
+  | AEPi Expr Expr
+  -- references are only allowed to bound idents
+  | AERefOf Natural
+  -- a reference type contains both the scope in which the referenced variable originated
+  -- (from the top of the stack so we know when it gets invalidated),
+  -- and also the type of what's referenced
+  -- | AERefOfTy Natural
+  deriving (Eq, Generic)
+instance Hashable AtomicExpr
+
+-- NOTE: these patterns don't allow nesting (to avoid the need for propagation of that)
+data PatternInf = PatIgnore | PatFull
+  deriving (Eq, Generic)
+instance Hashable PatternInf
+
+data Expr =
+    EAtomic AtomicExpr
+  | EApply  AtomicExpr AtomicExpr [AtomicExpr]
+  -- we allow atomic expr's to be let bound because we need to be able to take references to them
+  | ELet { elpat :: PatternInf, elval :: Expr, elbody :: Expr }
+  deriving (Eq, Generic)
+instance Hashable Expr
+
+patAllocSlots :: PatternInf -> Natural
+patAllocSlots pat = case pat of
+    PatIgnore -> 0
+    PatFull   -> 1
+
+-- evaluation and quoting
+
+data NeutralRoot = NrLiteral Literal
+  | Local Natural
+  | Quote Natural
+  deriving (Eq, Generic)
+instance Hashable NeutralRoot
+
+data Neutral = Neutral NeutralRoot [Value]
+
+data EvalError =
+    EEInvalidApply Value Value
+  | EEOutOfRange Natural
+
+type EvalResult a = Either EvalError a
+type EvalMonad  a = ReaderT [Value] (Either EvalError) a
+
+data Value = VLam (Value -> EvalResult Value)
+  | VPi Value (Value -> EvalResult Value)
+  | VNeutral Neutral
+  -- when using a reference when the value was expected (or the other way around)
+  -- an error should be raised
+  | VRefOf   Value
+  | VRefOfTy Natural Value
+
+vapp :: Value -> [Value] -> EvalResult Value
+vapp v [] = Right v
+vapp (VLam l) (v:xs) = l v >>= \res -> vapp res xs
+-- NOTE: this allows cases where a lambda violates borrowing rules
+vapp (VRefOf r) xs = vapp r     xs
+vapp v (x:_) = Left $ EEInvalidApply v x
+
+evalAtomic :: AtomicExpr -> EvalMonad Value
+evalAtomic eat = case eat of
+  AELiteral  l -> pure . VNeutral $ Neutral (NrLiteral l) []
+  AELambda   l -> asks (\env -> VLam $ \x -> eval l (x:env))
+  AEPi arg ret -> do
+    env <- ask
+    arg' <- eval' arg
+    pure $ VPi arg' $ \x -> eval ret (x:env)
+
+  AEBound    b -> lb' b
+  AERefOf    b -> fmap VRefOf $ lb' b
+
+  where
+    lb' :: Natural -> EvalMonad Value
+    lb' b = ReaderT $ lb'' b
+
+    lb'' :: Natural -> [Value] -> EvalResult Value
+    lb'' b env = case lookupBinder env b of
+      Nothing -> Left $ EEOutOfRange b
+      Just x   -> Right x
+
+eval' :: Expr -> EvalMonad Value
+eval' (EAtomic eat) = evalAtomic eat
+
+eval' (EApply eat rhs rhsxs) = do
+  eat' <- evalAtomic eat
+  rhs' <- evalAtomic rhs
+  rhsxs' <- sequenceA $ fmap evalAtomic rhsxs
+  ReaderT $ \_ -> vapp eat' $ rhs' : rhsxs'
+
+eval' (ELet { elpat = PatIgnore, elval = _, elbody = elb }) = eval' elb
+
+eval' (ELet { elpat = PatFull, elval = elv, elbody = elb }) = do
+  elval' <- eval' elv
+  local (\env -> (elval':env)) $ eval' elb
+
+eval :: Expr -> [Value] -> EvalResult Value
+eval e = runReaderT $ eval' e

haskell/nfker7h/lib/Language/Yanais/Nfker7h/Ast.hs

@@ -14,7 +14,6 @@ module Language.Yanais.Nfker7h.Ast (
     ValueError(..),
     Value(..),
 
-    binderLookup,
     eval,
     subst,
 
@@ -24,7 +23,7 @@ module Language.Yanais.Nfker7h.Ast (
 ) where
 
 import Control.Monad.Reader (Reader, MonadReader(..))
-import Data.Hashable (Hashable)
+-- import Data.Hashable (Hashable)
 import Data.Void (Void, absurd)
 import qualified Deque.Strict as Deq
 import Generic.Data (Generic)
@@ -32,21 +31,7 @@ import Numeric.Natural (Natural)
 
 import Language.Yanais.Parser.Lex (Ident, nullIdent)
 import Language.Yanais.Nfker7h.Pattern (Pattern(..))
-
--- | integer sizes
-data IntSz = PI8 | PI16 | PI32 | PI64 | PIsize
-    deriving (Show, Eq, Generic)
-instance Hashable IntSz
-
--- | primitive type literals
-data PrimTy = PtType | PtBool | PtString | PtIntSz | PtUnsInt IntSz | PtSigInt IntSz
-  deriving (Show, Eq, Generic)
-instance Hashable PrimTy
-
--- | all possible literals
-data Literal = LPrimTy PrimTy | LIntSz IntSz | LNat Natural
-  deriving (Show, Eq, Generic)
-instance Hashable Literal
+import Language.Yanais.Nfker7h.Literal
 
 data NeutralRoot = NrLiteral Literal
   | Global Ident
@@ -103,12 +88,6 @@ data Value = VLam (Value -> Either ValueError Value)
   | VRefOf   Value
   | VRefOfTy Value
 
-binderLookup :: [a] -> Natural -> Maybe a
-binderLookup = foldr ffun (const Nothing)
-  where
-    ffun x _ 0 = Just x
-    ffun _ r k = r (k-1)
-
 vapp :: Value -> Value -> Either ValueError Value
 vapp (VLam f) v = f v
 vapp (VRefOf r) v = vapp r v
@@ -131,7 +110,7 @@ unpackVP val bindpat env = case bindpat of
 -- | evaluate an expression in an environment
 eval :: Expr info -> EvalEnv -> Either ValueError Value
 eval (Expr _ kind) env = case kind of
-  EBound     b    -> case binderLookup env b of
+  EBound     b    -> case lookupBinder env b of
     Nothing -> Left . VEOutOfRange $ b
     Just y  -> Right y
   EFree      x    -> Right. VNeutral $ Neutral x mempty

haskell/nfker7h/lib/Language/Yanais/Nfker7h/Literal.hs

@@ -0,0 +1,38 @@
+{-# LANGUAGE DeriveFunctor, DeriveGeneric #-}
+
+module Language.Yanais.Nfker7h.Literal (
+    IntSz(..),
+    PrimTy(..),
+    Literal(..),
+
+    lookupBinder,
+) where
+
+import Data.Hashable (Hashable)
+import Generic.Data (Generic)
+import Numeric.Natural (Natural)
+
+-- import Language.Yanais.Parser.Lex (Ident, nullIdent)
+
+-- | integer sizes
+data IntSz = PI8 | PI16 | PI32 | PI64 | PIsize
+    deriving (Show, Eq, Generic)
+instance Hashable IntSz
+
+-- | primitive type literals
+data PrimTy = PtType | PtBool | PtString | PtIntSz | PtUnsInt IntSz | PtSigInt IntSz
+  deriving (Show, Eq, Generic)
+instance Hashable PrimTy
+
+-- | all possible literals
+data Literal = LPrimTy PrimTy | LIntSz IntSz | LNat Natural
+  deriving (Show, Eq, Generic)
+instance Hashable Literal
+
+-- | lookup a value in a list by its position (via Natural instead of Int);
+-- this is only here because it has no dependencies
+lookupBinder :: [a] -> Natural -> Maybe a
+lookupBinder = foldr ffun (const Nothing)
+  where
+    ffun x _ 0 = Just x
+    ffun _ r k = r (k-1)

haskell/nfker7h/lib/Language/Yanais/Nfker7h/Typeck.hs

@@ -12,6 +12,7 @@ import Numeric.Natural
 
 import Language.Yanais.Parser.Lex (nullIdent)
 import Language.Yanais.Nfker7h.Ast
+import Language.Yanais.Nfker7h.Literal (lookupBinder)
 import Language.Yanais.Nfker7h.Pattern (Pattern(..))
 
 data TyckEnv = TyckEnv {
@@ -32,8 +33,8 @@ data TypeError = TETypesNotEq (Expr ()) (Expr ())
 
 type TyckMonad a = ReaderT TyckEnv (Either TypeError) a
 
-binderLookup' :: Natural -> TyckMonad Value
-binderLookup' n = ReaderT $ \env -> case binderLookup (binders env) n of
+lookupBinder' :: Natural -> TyckMonad Value
+lookupBinder' n = ReaderT $ \env -> case lookupBinder (binders env) n of
   Nothing -> Left . TEValueError $ VEOutOfRange n
   Just x  -> Right x
 
@@ -53,10 +54,10 @@ typeChkIsTy e = typeChk e $ litToVal $ LPrimTy PtType
 
 typeInf :: Expr () -> TyckMonad Type
 typeInf (Expr _ kind) = case kind of
-  EBound n -> binderLookup' n
+  EBound n -> lookupBinder' n
 
   -- TODO: get rid of this case
-  EFree (Local n) -> binderLookup' n
+  EFree (Local n) -> lookupBinder' n
 
   EFree (NrLiteral l) ->
     let tau = NrLiteral . LPrimTy $ case l of

haskell/nfker7h/yanais-nfker7h.cabal

@@ -60,7 +60,9 @@ library
 
     -- Modules exported by the library.
     exposed-modules:
-        Language.Yanais.Nfker7h.Ast
+        Language.Yanais.Nfker7h.Anf
+      , Language.Yanais.Nfker7h.Ast
+      , Language.Yanais.Nfker7h.Literal
       , Language.Yanais.Nfker7h.Pattern
       , Language.Yanais.Nfker7h.Typeck
       , Language.Yanais.Nfker7h.Parser.Types