Initial commit.

.envrc

@@ -0,0 +1 @@
+use flake

.gitignore

@@ -0,0 +1,35 @@
+# direnv
+*.sw?
+.direnv
+.gopath
+/direnv
+/direnv.test
+/dist
+/test/config
+/test/data
+/test/scenarios/inherited/.envrc
+
+# haskell
+dist
+dist-*
+cabal-dev
+*.o
+*.hi
+*.hie
+*.chi
+*.chs.h
+*.dyn_o
+*.dyn_hi
+.hpc
+.hsenv
+.cabal-sandbox/
+cabal.sandbox.config
+*.prof
+*.aux
+*.hp
+*.eventlog
+.stack-work/
+cabal.project.local
+cabal.project.local~
+.HTF/
+.ghc.environment.*

cabal.project

@@ -0,0 +1,5 @@
+packages:
+  leibniz-proof
+  parser-adt
+  parser-closed
+  parser-gadt

flake.lock

@@ -0,0 +1,43 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "locked": {
+        "lastModified": 1638122382,
+        "narHash": "sha256-sQzZzAbvKEqN9s0bzWuYmRaA03v40gaJ4+iL1LXjaeI=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "74f7e4319258e287b0f9cb95426c9853b282730b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1639161226,
+        "narHash": "sha256-75Y08ynJDTq6HHGIF+8IADBJSVip0UyWQH7jqSFnRR8=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "573095944e7c1d58d30fc679c81af63668b54056",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixos-21.11",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

flake.nix

@@ -0,0 +1,21 @@
+{
+  description = "Code samples for `Tagless Final Variables`.";
+
+  inputs = {
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-21.11";
+    flake-utils.url = "github:numtide/flake-utils";
+  };
+
+  outputs = { self, nixpkgs, flake-utils }:
+    flake-utils.lib.eachDefaultSystem (system:
+      let
+        pkgs = nixpkgs.legacyPackages.${system};
+      in {
+        devShell = pkgs.mkShell {
+          buildInputs = [
+            pkgs.haskellPackages.cabal-install
+            pkgs.haskellPackages.ghc
+          ];
+        };
+      });
+}

leibniz-proof/app/Main.hs

@@ -0,0 +1,28 @@
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Main where
+
+import Data.Eq.Type ((:=)(..), refl)
+
+newtype F1 t b a = F1 {runF1 :: t := (a -> b)}
+newtype F2 t a b = F2 {runF2 :: t := (a -> b)}
+
+functionEquality
+  :: forall a1 a2 b1 b2
+   . a1 := a2
+  -> b1 := b2
+  -> (a1 -> b1) := (a2 -> b2)
+functionEquality
+  (Refl s1)  -- s1 :: forall c. c a1 -> c a2
+  (Refl s2)  -- s2 :: forall c. c b1 -> c b2
+  = runF2    -- (a1 -> b1) := (a2 -> b2)
+  . s2       -- F2 (a1 -> b1) a2 b2
+  . F2       -- F2 (a1 -> b1) a2 b1
+  . runF1    -- (a1 -> b1) := (a2 -> b1)
+  . s1       -- F1 (a1 -> b1) b1 a2
+  . F1       -- F1 (a1 -> b1) b1 a1
+  $ refl     -- (a1 -> b1) := (a1 -> b1)
+
+main :: IO ()
+main = putStrLn "Hello, Haskell!"

leibniz-proof/leibniz-proof.cabal

@@ -0,0 +1,10 @@
+  cabal-version:      3.4
+  name:               leibniz-proof
+  version:            0.1.0.0
+
+executable leibniz-proof
+  main-is:            Main.hs
+  build-depends:      base ^>=4.14.3.0,
+                      eq
+  hs-source-dirs:     app
+  default-language:   Haskell2010

parser-adt/app/Main.hs

@@ -0,0 +1,200 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Main where
+
+import qualified Control.Monad.Combinators.Expr as E
+import qualified Text.Megaparsec as M
+import qualified Text.Megaparsec.Char as MC
+import qualified Text.Megaparsec.Char.Lexer as ML
+
+import Control.Applicative ((<|>))
+import Control.DeepSeq (NFData(..), deepseq)
+import Control.Monad.State (MonadState, modify)
+import Control.Monad.Trans.Class (lift)
+import Control.Monad.Trans.Either (hoistEither)
+import Control.Monad.Trans.Except (ExceptT, runExceptT)
+import Data.Char (isDigit)
+import Data.Foldable (foldl')
+import Data.Functor (($>), void)
+import Data.Maybe (isJust)
+import Data.Text (Text, unpack)
+import Data.Text.IO (hGetContents)
+import Data.Void (Void)
+import Numeric (readDec)
+import System.Environment (getArgs)
+import System.IO (IOMode(ReadMode), openFile)
+
+-- ========================================
+-- ADT
+-- ========================================
+
+data Expr
+  = EInt  Integer
+  | EBool Bool
+  | EAdd  Expr Expr
+  | ESub  Expr Expr
+  | EAnd  Expr Expr
+  | EOr   Expr Expr
+  deriving (Show)
+
+eval :: Expr -> Either Text Expr
+eval e@(EInt  _) = pure e
+eval e@(EBool _) = pure e
+eval (EAdd lhs rhs) = do
+  (lhs', rhs') <- binInt lhs rhs
+  pure $ EInt (lhs' + rhs')
+eval (ESub lhs rhs) = do
+  (lhs', rhs') <- binInt lhs rhs
+  pure $ EInt (lhs' - rhs')
+eval (EAnd lhs rhs) = do
+  (lhs', rhs') <- binBool lhs rhs
+  pure $ EBool (lhs' && rhs')
+eval (EOr lhs rhs) = do
+  (lhs', rhs') <- binBool lhs rhs
+  pure $ EBool (lhs' || rhs')
+
+binInt :: Expr -> Expr -> Either Text (Integer, Integer)
+binInt lhs rhs = do
+  lhs' <- eval lhs
+  rhs' <- eval rhs
+  case (lhs', rhs') of
+    (EInt lhs'', EInt rhs'') -> pure (lhs'', rhs'')
+    _ -> Left "Expected two integers."
+
+binBool :: Expr -> Expr -> Either Text (Bool, Bool)
+binBool lhs rhs = do
+  lhs' <- eval lhs
+  rhs' <- eval rhs
+  case (lhs', rhs') of
+    (EBool lhs'', EBool rhs'') -> pure (lhs'', rhs'')
+    _ -> Left "Expected two booleans."
+
+-- ========================================
+-- Lexers
+-- ========================================
+
+type Parser = M.Parsec Void Text
+
+space :: Parser ()
+space = ML.space MC.space1 M.empty M.empty
+{-# INLINE space #-}
+
+lexeme :: forall a. Parser a -> Parser a
+lexeme = ML.lexeme MC.space
+{-# INLINE lexeme #-}
+
+symbol :: Text -> Parser Text
+symbol = ML.symbol space
+{-# INLINE symbol #-}
+
+parens :: forall a. Parser a -> Parser a
+parens = M.between (symbol "(") (symbol ")")
+{-# INLINE parens #-}
+
+boolean :: Parser Bool
+boolean = lexeme $ MC.string "true" $> True <|> MC.string "false" $> False
+{-# INLINE boolean #-}
+
+integer :: Parser Integer
+integer = lexeme ML.decimal
+{-# INLINE integer #-}
+
+-- ========================================
+-- Naive attempt
+-- ========================================
+
+naiveExpr :: Parser Expr
+naiveExpr = E.makeExprParser term
+  [ [binary "+" EAdd, binary "-" ESub]
+  , [binary "&&" EAnd, binary "||" EOr]
+  ]
+ where
+  binary name f = E.InfixL (f <$ symbol name)
+
+  term = parens naiveExpr <|>
+         EInt <$> integer <|>
+         EBool <$> boolean
+
+-- ========================================
+-- Multiple passes
+-- ========================================
+
+mulPassExpr :: Parser Expr
+mulPassExpr = expr >>= either (fail . unpack) pure
+ where
+  expr = E.makeExprParser term
+    [ [binary "+"  binInt  EInt  EAdd, binary "-"  binInt  EInt  ESub]
+    , [binary "&&" binBool EBool EAnd, binary "||" binBool EBool EOr]
+    ]
+
+  binary name b f op = E.InfixL do
+    void $ symbol name
+    pure $ \lhs rhs -> do
+      lhs' <- lhs
+      rhs' <- rhs
+      (lhs', rhs') <- b lhs' rhs'
+      eval $ op (f lhs') (f rhs')
+
+  term = parens expr <|>
+         Right . EInt <$> integer <|>
+         Right . EBool <$> boolean
+
+-- ========================================
+-- Memory consumption
+-- ========================================
+
+instance NFData Expr where
+  rnf (EInt  e) = rnf e
+  rnf (EBool e) = rnf e
+  rnf (EAdd lhs rhs) = rnf lhs `seq` rnf rhs
+  rnf (ESub lhs rhs) = rnf lhs `seq` rnf rhs
+  rnf (EAnd lhs rhs) = rnf lhs `seq` rnf rhs
+  rnf (EOr  lhs rhs) = rnf lhs `seq` rnf rhs
+
+memConsExpr :: Parser Expr
+memConsExpr = do
+  e <- runExceptT $ term >>= expr
+  either (fail . unpack) pure e
+ where
+  expr :: Expr -> ExceptT Text Parser Expr
+  expr t = do
+    op <- lift $ M.option Nothing $ Just <$> M.choice
+      [symbol "+", symbol "-", symbol "&&", symbol "||"]
+    case op of
+      Just "+"  -> nest t EAdd
+      Just "-"  -> nest t ESub
+      Just "&&" -> nest t EAnd
+      Just "||" -> nest t EOr
+      _         -> pure t
+
+  nest t f = do
+    t' <- term
+    z <- hoistEither . eval $ f t t'
+    -- Need to reduce to NF for strictness guarantees.
+    z `deepseq` expr z
+
+  term = do
+    p <- lift $ M.option Nothing $ Just <$> (symbol "(")
+    if isJust p then (term >>= expr) <* lift (symbol ")") else
+      lift $ EInt <$> integer <|> EBool <$> boolean
+
+-- ========================================
+-- Main
+-- ========================================
+
+run :: FilePath -> IO ()
+run fileName = do
+  handle <- openFile fileName ReadMode
+  contents <- hGetContents handle
+  case M.parse (memConsExpr <* M.eof) fileName contents of
+    Left e -> print $ M.errorBundlePretty e
+    Right a -> print $ eval a
+
+main :: IO ()
+main = do
+  [fileName] <- getArgs
+  run fileName

parser-adt/parser-adt.cabal

@@ -0,0 +1,16 @@
+  cabal-version:      3.4
+  name:               parser-adt
+  version:            0.1.0.0
+
+executable parser-adt
+  main-is:            Main.hs
+  build-depends:      base ^>=4.14.3.0,
+                      deepseq,
+                      megaparsec,
+                      mtl,
+                      parser-combinators,
+                      text,
+                      transformers,
+                      transformers-either
+  hs-source-dirs:     app
+  default-language:   Haskell2010

parser-closed/app/Main.hs

@@ -0,0 +1,199 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module Main where
+
+import qualified Control.Monad.Combinators.Expr as E
+import qualified Data.Eq.Type as EQ
+import qualified Text.Megaparsec as M
+import qualified Text.Megaparsec.Char as MC
+import qualified Text.Megaparsec.Char.Lexer as ML
+
+import Control.Applicative ((<|>))
+import Data.Char (isDigit)
+import Data.Eq.Type ((:=))
+import Data.Foldable (foldl')
+import Data.Functor (($>), void)
+import Data.Proxy (Proxy(..))
+import Data.Text (Text, unpack)
+import Data.Text.IO (hGetContents)
+import Data.Void (Void)
+import Numeric (readDec)
+import System.Environment (getArgs)
+import System.IO (IOMode(ReadMode), openFile)
+
+-- ========================================
+-- Symantics
+-- ========================================
+
+class Symantics repr where
+  eInt  :: Integer -> repr Integer
+  eBool :: Bool -> repr Bool
+  eAdd  :: repr Integer -> repr Integer -> repr Integer
+  eSub  :: repr Integer -> repr Integer -> repr Integer
+  eAnd  :: repr Bool -> repr Bool -> repr Bool
+  eOr   :: repr Bool -> repr Bool -> repr Bool
+
+newtype SQ a = SQ {runSQ :: forall repr. Symantics repr => repr a}
+
+instance Symantics SQ where
+  eInt  e = SQ (eInt e)
+  eBool e = SQ (eBool e)
+  eAdd (SQ lhs) (SQ rhs) = SQ (eAdd lhs rhs)
+  eSub (SQ lhs) (SQ rhs) = SQ (eSub lhs rhs)
+  eAnd (SQ lhs) (SQ rhs) = SQ (eAnd lhs rhs)
+  eOr  (SQ lhs) (SQ rhs) = SQ (eOr  lhs rhs)
+
+newtype Expr a = Expr {runExpr :: a} deriving Show
+
+instance Symantics Expr where
+  eInt  = Expr
+  eBool = Expr
+  eAdd (Expr lhs) (Expr rhs) = Expr (lhs + rhs)
+  eSub (Expr lhs) (Expr rhs) = Expr (lhs - rhs)
+  eAnd (Expr lhs) (Expr rhs) = Expr (lhs && rhs)
+  eOr  (Expr lhs) (Expr rhs) = Expr (lhs || rhs)
+
+-- ========================================
+-- Typeable
+-- ========================================
+
+class Typeable repr where
+  pInt  :: repr Integer
+  pBool :: repr Bool
+
+newtype TQ t = TQ {runTQ :: forall repr. Typeable repr => repr t}
+
+instance Typeable TQ where
+  pInt  = TQ pInt
+  pBool = TQ pBool
+
+newtype AsInt a = AsInt (Maybe (a := Integer))
+
+instance Typeable AsInt where
+  pInt  = AsInt (Just EQ.refl)
+  pBool = AsInt Nothing
+
+newtype AsBool a = AsBool (Maybe (a := Bool))
+
+instance Typeable AsBool where
+  pInt  = AsBool Nothing
+  pBool = AsBool (Just EQ.refl)
+
+-- ========================================
+-- Dynamic
+-- ========================================
+
+data Dynamic repr = forall t. Dynamic (TQ t) (repr t)
+
+class IsDynamic a where
+  type' :: forall repr. Typeable repr => repr a
+  lift' :: forall repr. Symantics repr => a -> repr a
+  cast' :: forall repr t. TQ t -> Maybe (t := a)
+
+instance IsDynamic Integer where
+  type' = pInt
+  lift' = eInt
+  cast' (TQ t) = case t of AsInt a -> a
+
+instance IsDynamic Bool where
+  type' = pBool
+  lift' = eBool
+  cast' (TQ t) = case t of AsBool a -> a
+
+toDyn :: forall repr a. IsDynamic a => Symantics repr => a -> Dynamic repr
+toDyn = Dynamic type' . lift'
+
+fromDyn :: forall repr a. IsDynamic a => Dynamic repr -> Maybe (repr a)
+fromDyn (Dynamic t e) = case t of
+  (cast' -> r) -> do
+    r' <- r
+    pure $ EQ.coerce (EQ.lift r') e
+
+-- ========================================
+-- Parser code
+-- ========================================
+
+type Parser = M.Parsec Void Text
+
+space :: Parser ()
+space = ML.space MC.space1 M.empty M.empty
+{-# INLINE space #-}
+
+lexeme_ :: forall a. Parser a -> Parser a
+lexeme_ = ML.lexeme $ MC.space1 <|> M.eof
+{-# INLINE lexeme_ #-}
+
+symbol :: Text -> Parser Text
+symbol = ML.symbol space
+{-# INLINE symbol #-}
+
+parens :: forall a. Parser a -> Parser a
+parens = M.between (symbol "(") (symbol ")")
+{-# INLINE parens #-}
+
+boolean :: Parser Bool
+boolean = lexeme_ do
+  MC.string "true" $> True <|> MC.string "false" $> False
+{-# INLINE boolean #-}
+
+integer :: Parser Integer
+integer = lexeme_ do
+  i <- M.some $ M.satisfy isDigit
+  case readDec i of
+    [(value, "")] -> pure value
+    _ -> fail "integer"
+{-# INLINE integer #-}
+
+mkBinary
+  :: forall repr a
+   . Symantics repr
+  => IsDynamic a
+  => (repr a -> repr a -> repr a)
+  -> Dynamic repr
+  -> Dynamic repr
+  -> Maybe (Dynamic repr)
+mkBinary bin lhs rhs = do
+  lhs' <- fromDyn lhs
+  rhs' <- fromDyn rhs
+  pure . Dynamic type' $ bin lhs' rhs'
+
+expr :: forall repr. Symantics repr => Parser (Dynamic repr)
+expr = expr' >>= \case
+  Left (offset, msg) -> M.setOffset offset >> fail msg
+  Right a -> pure a
+ where
+  expr' = E.makeExprParser
+    (parens expr' <|> Right . toDyn <$> integer <|> Right . toDyn <$> boolean)
+    [ [binary' "+" eAdd, binary' "-" eSub]
+    , [binary' "&&" eAnd, binary' "||" eOr]
+    ]
+
+  binary' name bin = E.InfixL do
+    void $ symbol name
+    offset <- M.getOffset
+    pure $ \lhs rhs -> do
+      lhs' <- lhs
+      rhs' <- rhs
+      case mkBinary bin lhs' rhs' of
+        Nothing -> Left (offset, "Invalid operands for `" <> unpack name <> "`")
+        Just a -> pure a
+
+-- ========================================
+-- Main
+-- ========================================
+
+main :: IO ()
+main = do
+  [fileName] <- getArgs
+  handle <- openFile fileName ReadMode
+  contents <- hGetContents handle
+  case M.parse expr fileName contents of
+    Left e -> print $ M.errorBundlePretty e
+    Right a -> print (fromDyn a :: Maybe (Expr Integer))

parser-closed/parser-closed.cabal

@@ -0,0 +1,13 @@
+  cabal-version:      3.4
+  name:               parser-closed
+  version:            0.1.0.0
+
+executable parser-closed
+  main-is:          Main.hs
+  build-depends:    base ^>=4.14.3.0,
+                    eq,
+                    megaparsec,
+                    parser-combinators,
+                    text
+  hs-source-dirs:   app
+  default-language: Haskell2010

parser-gadt/app/Main.hs

@@ -0,0 +1,116 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE StandaloneDeriving #-}
+
+module Main where
+
+import qualified Control.Monad.Combinators.Expr as E
+import qualified Text.Megaparsec as M
+import qualified Text.Megaparsec.Char as MC
+import qualified Text.Megaparsec.Char.Lexer as ML
+
+import Control.Applicative ((<|>))
+import Data.Char (isDigit)
+import Data.Foldable (foldl')
+import Data.Functor (($>))
+import Data.Text (Text)
+import Data.Void (Void)
+import Numeric (readDec)
+import System.Environment (getArgs)
+
+-- ========================================
+-- GADT
+-- ========================================
+
+data Expr a where
+  EInt  :: Integer -> Expr Integer
+  EBool :: Bool -> Expr Bool
+  EAdd  :: Expr Integer -> Expr Integer -> Expr Integer
+  ESub  :: Expr Integer -> Expr Integer -> Expr Integer
+  EAnd  :: Expr Bool -> Expr Bool -> Expr Bool
+  EOr   :: Expr Bool -> Expr Bool -> Expr Bool
+
+deriving instance Show (Expr Integer)
+deriving instance Show (Expr Bool)
+
+eval :: forall a. Expr a -> Either Bool Integer
+eval (EInt e) = Right e
+eval (EBool e) = Left e
+eval (EAdd lhs rhs) =
+  let Right r1 = eval lhs
+      Right r2 = eval rhs
+   in Right (r1 + r2)
+eval (ESub lhs rhs) =
+  let Right r1 = eval lhs
+      Right r2 = eval rhs
+   in Right (r1 - r2)
+eval (EAnd lhs rhs) =
+  let Left r1 = eval lhs
+      Left r2 = eval rhs
+   in Left (r1 && r2)
+eval (EOr lhs rhs) =
+  let Left r1 = eval lhs
+      Left r2 = eval rhs
+   in Left (r1 || r2)
+
+-- ========================================
+-- Unused parser code
+-- ========================================
+
+type Parser = M.Parsec Void Text
+
+space :: Parser ()
+space = ML.space MC.space1 M.empty M.empty
+{-# INLINE space #-}
+
+lexeme_ :: forall a. Parser a -> Parser a
+lexeme_ = ML.lexeme $ MC.space1 <|> M.eof
+{-# INLINE lexeme_ #-}
+
+symbol :: Text -> Parser Text
+symbol = ML.symbol space
+{-# INLINE symbol #-}
+
+parens :: forall a. Parser a -> Parser a
+parens = M.between (symbol "(") (symbol ")")
+{-# INLINE parens #-}
+
+boolean :: Parser Bool
+boolean = lexeme_ do
+  MC.string "true" $> True <|> MC.string "false" $> False
+{-# INLINE boolean #-}
+
+integer :: Parser Integer
+integer = lexeme_ do
+  i <- M.some $ M.satisfy isDigit
+  case readDec i of
+    [(value, "")] -> pure value
+    _ -> fail "integer"
+{-# INLINE integer #-}
+
+{-
+Couldn't match type `Bool` with `Integer`
+
+parseExpr = E.makeExprParser parseTerm
+  [ [binary "+" EAdd, binary "-" ESub]
+  , [binary "&&" EAnd, binary "||" EOr]
+  ]
+ where
+  binary name f = E.InfixL  (f <$ symbol name)
+  parseTerm = parens parseExpr <|>
+              EInt <$> integer <|>
+              EBool <$> boolean
+-}
+
+-- ========================================
+-- Main
+-- ========================================
+
+main :: IO ()
+main = do
+  [count] <- map read <$> getArgs
+  let expr = foldl' EAdd (EInt 0) $ take count (EInt <$> [1..])
+  print $ {-# SCC "evaluated" #-} eval expr

parser-gadt/parser-gadt.cabal

@@ -0,0 +1,12 @@
+  cabal-version:      3.4
+  name:               parser-gadt
+  version:            0.1.0.0
+
+executable parser-gadt
+  main-is:            Main.hs
+  build-depends:      base ^>=4.14.3.0,
+                      megaparsec,
+                      parser-combinators,
+                      text
+  hs-source-dirs:     app
+  default-language:   Haskell2010