commit c69f000ebe108eb70553e7f616650b451fdfa84b Author: Joshua Potter Date: Mon Dec 20 08:16:50 2021 -0500 Initial commit. diff --git a/.envrc b/.envrc new file mode 100644 index 0000000..3550a30 --- /dev/null +++ b/.envrc @@ -0,0 +1 @@ +use flake diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..d4bfdbc --- /dev/null +++ b/.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.* diff --git a/cabal.project b/cabal.project new file mode 100644 index 0000000..0d89d56 --- /dev/null +++ b/cabal.project @@ -0,0 +1,5 @@ +packages: + leibniz-proof + parser-adt + parser-closed + parser-gadt diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..6bcee1d --- /dev/null +++ b/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 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..e76d1b5 --- /dev/null +++ b/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 + ]; + }; + }); +} diff --git a/leibniz-proof/app/Main.hs b/leibniz-proof/app/Main.hs new file mode 100644 index 0000000..95e6688 --- /dev/null +++ b/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!" diff --git a/leibniz-proof/leibniz-proof.cabal b/leibniz-proof/leibniz-proof.cabal new file mode 100644 index 0000000..ad24011 --- /dev/null +++ b/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 diff --git a/parser-adt/app/Main.hs b/parser-adt/app/Main.hs new file mode 100644 index 0000000..9b11541 --- /dev/null +++ b/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 diff --git a/parser-adt/parser-adt.cabal b/parser-adt/parser-adt.cabal new file mode 100644 index 0000000..3d4ea9c --- /dev/null +++ b/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 diff --git a/parser-closed/app/Main.hs b/parser-closed/app/Main.hs new file mode 100644 index 0000000..806658d --- /dev/null +++ b/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)) diff --git a/parser-closed/parser-closed.cabal b/parser-closed/parser-closed.cabal new file mode 100644 index 0000000..03f0c8a --- /dev/null +++ b/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 diff --git a/parser-gadt/app/Main.hs b/parser-gadt/app/Main.hs new file mode 100644 index 0000000..c597627 --- /dev/null +++ b/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 diff --git a/parser-gadt/parser-gadt.cabal b/parser-gadt/parser-gadt.cabal new file mode 100644 index 0000000..9c81aed --- /dev/null +++ b/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