Complexity was getting out of hand. Beginning a rewrite. Added tests.
parent
807a0cb1ee
commit
25658f370a
GPG Key ID:
4B7F3DA9351E577C
@ -1,3 +1,3 @@
|
||||
.stack-work/
|
||||
untyped-lambda-calculus.cabal
|
||||
*~
|
||||
*.cabal
|
||||
*~
|
||||
|
||||
@ -1,70 +0,0 @@
|
||||
cabal-version: 1.12
|
||||
|
||||
-- This file has been generated from package.yaml by hpack version 0.31.2.
|
||||
--
|
||||
-- see: https://github.com/sol/hpack
|
||||
--
|
||||
-- hash: 26600940e6acf0bd4e6fbb02d188b88fd368836effa5ea0427f7a4d5cd792669
|
||||
|
||||
name: jtm-lambda-calculus
|
||||
version: 0.1.0.0
|
||||
synopsis: Implementations of various Lambda Calculus evaluators and type systems.
|
||||
description: Please see the README on GitHub at <https://github.com/jamestmartin/lambda-calculus#readme>
|
||||
category: LambdaCalculus
|
||||
homepage: https://github.com/jamestmartin/lambda-calculus#readme
|
||||
bug-reports: https://github.com/jamestmartin/lambda-calculus/issues
|
||||
author: James Martin
|
||||
maintainer: james@jtmar.me
|
||||
copyright: 2019 James Martin
|
||||
license: GPL-3
|
||||
license-file: LICENSE
|
||||
build-type: Simple
|
||||
extra-source-files:
|
||||
README.md
|
||||
|
||||
source-repository head
|
||||
type: git
|
||||
location: https://github.com/jamestmartin/lambda-calculus
|
||||
|
||||
library
|
||||
exposed-modules:
|
||||
Data.Type.Nat
|
||||
Data.Vec
|
||||
LambdaCalculus.Combinators
|
||||
LambdaCalculus.Evaluation.Optimal
|
||||
LambdaCalculus.Parser
|
||||
LambdaCalculus.Representation
|
||||
LambdaCalculus.Representation.AbstractSyntax
|
||||
LambdaCalculus.Representation.Dependent.ReverseDeBruijn
|
||||
LambdaCalculus.Representation.Standard
|
||||
other-modules:
|
||||
Paths_jtm_lambda_calculus
|
||||
hs-source-dirs:
|
||||
src
|
||||
default-extensions: BlockArguments DataKinds DeriveFoldable DeriveFunctor DeriveTraversable FlexibleInstances FunctionalDependencies GADTs KindSignatures LambdaCase MultiParamTypeClasses PolyKinds Rank2Types TemplateHaskell TypeFamilies TypeOperators
|
||||
build-depends:
|
||||
base >=4.7 && <5
|
||||
, free >=5.1 && <6
|
||||
, mtl >=2.2 && <3
|
||||
, parsec >=3.1 && <4
|
||||
, recursion-schemes >=5.1 && <6
|
||||
, unordered-containers >=0.2.10 && <0.3
|
||||
default-language: Haskell2010
|
||||
|
||||
executable jtm-lambda-calculus-exe
|
||||
main-is: Main.hs
|
||||
other-modules:
|
||||
Paths_jtm_lambda_calculus
|
||||
hs-source-dirs:
|
||||
app
|
||||
default-extensions: BlockArguments DataKinds DeriveFoldable DeriveFunctor DeriveTraversable FlexibleInstances FunctionalDependencies GADTs KindSignatures LambdaCase MultiParamTypeClasses PolyKinds Rank2Types TemplateHaskell TypeFamilies TypeOperators
|
||||
ghc-options: -threaded -rtsopts -with-rtsopts=-N
|
||||
build-depends:
|
||||
base >=4.7 && <5
|
||||
, free >=5.1 && <6
|
||||
, jtm-lambda-calculus
|
||||
, mtl >=2.2 && <3
|
||||
, parsec >=3.1 && <4
|
||||
, recursion-schemes >=5.1 && <6
|
||||
, unordered-containers >=0.2.10 && <0.3
|
||||
default-language: Haskell2010
|
||||
@ -1,54 +0,0 @@
|
||||
-- | I would rather depend on the `fin` package than export my own Nat type,
|
||||
-- but I couldn't figure out how to write substitution with their definition of SNat,
|
||||
-- because it uses `SNatI n =>` instead of `SNat n ->` in the recursive case,
|
||||
-- and `withSNat` and `snat` were both providing ambigous type variables and all that.
|
||||
-- If anyone could fix it for me, I would gladly accept a PR.
|
||||
module Data.Type.Nat where
|
||||
|
||||
import Data.Type.Equality ((:~:)(Refl))
|
||||
import Numeric.Natural (Natural)
|
||||
|
||||
data Nat = Z | S Nat
|
||||
|
||||
instance Show Nat where
|
||||
show = show . natToNatural
|
||||
|
||||
data SNat :: Nat -> * where
|
||||
SZ :: SNat 'Z
|
||||
SS :: SNat n -> SNat ('S n)
|
||||
|
||||
instance Show (SNat n) where
|
||||
show = show . snatToNatural
|
||||
|
||||
type family Plus (n :: Nat) (m :: Nat) = (sum :: Nat) where
|
||||
Plus Z m = m
|
||||
Plus ('S n) m = 'S (Plus n m)
|
||||
|
||||
class SNatI (n :: Nat) where snat :: SNat n
|
||||
instance SNatI 'Z where snat = SZ
|
||||
instance SNatI n => SNatI ('S n) where snat = SS snat
|
||||
|
||||
natToNatural :: Nat -> Natural
|
||||
natToNatural Z = 0
|
||||
natToNatural (S n) = 1 + natToNatural n
|
||||
|
||||
snatToNat :: forall n. SNat n -> Nat
|
||||
snatToNat SZ = Z
|
||||
snatToNat (SS n) = S $ snatToNat n
|
||||
|
||||
snatToNatural :: forall n. SNat n -> Natural
|
||||
snatToNatural = natToNatural . snatToNat
|
||||
|
||||
plusZero :: SNat n -> Plus n 'Z :~: n
|
||||
-- trivial: Z + n = n by definition of equality,
|
||||
-- and in this case n = Z and thus Z + Z = Z.
|
||||
plusZero SZ = Refl
|
||||
-- if n + Z = n, then S n + Z = S n.
|
||||
plusZero (SS n) = case plusZero n of Refl -> Refl
|
||||
|
||||
plusSuc :: SNat n -> SNat m -> Plus n ('S m) :~: 'S (Plus n m)
|
||||
-- trivial: Z + n = n by definition of equality,
|
||||
-- and in this case n = S m, and thus Z + S m = S m.
|
||||
plusSuc SZ _ = Refl
|
||||
-- if n + S m = S (n + m), then S n + S m = S (S n + m).
|
||||
plusSuc (SS n) m = case plusSuc n m of Refl -> Refl
|
||||
@ -1,8 +0,0 @@
|
||||
module Data.Vec where
|
||||
|
||||
import Data.Type.Nat
|
||||
|
||||
-- | See the documentation of 'Data.Type.Nat' to see why I don't just depend on the `vec` package.
|
||||
data Vec :: Nat -> * -> * where
|
||||
VNil :: Vec 'Z a
|
||||
(:::) :: a -> Vec n a -> Vec ('S n) a
|
||||
@ -1,8 +0,0 @@
|
||||
module LambdaCalculus.Combinators where
|
||||
|
||||
import LambdaCalculus.Representation (IsExpr, fromStandard)
|
||||
import LambdaCalculus.Representation.Standard
|
||||
|
||||
-- | The `I` combinator, representing the identify function `λx. x`.
|
||||
i :: IsExpr expr => expr
|
||||
i = fromStandard $ Abstraction "x" $ Variable "x"
|
||||
@ -1,175 +0,0 @@
|
||||
-- | !!!IMPORTANT!!!
|
||||
-- This module is a WORK IN PROGRESS.
|
||||
-- It DOES NOT YET IMPLEMENT OPTIMAL EVALUATION.
|
||||
-- It currently implements *lazy* evaluation with the reverse de bruijn syntax,
|
||||
-- and my end goal is to make it support optimal evaluation,
|
||||
-- but currently it is not even close.
|
||||
module LambdaCalculus.Evaluation.Optimal where
|
||||
|
||||
import Control.Applicative ((<|>))
|
||||
import Data.Type.Nat
|
||||
import LambdaCalculus.Representation.Dependent.ReverseDeBruijn
|
||||
|
||||
-- | The meaning of expressions is defined by how they can be reduced.
|
||||
-- There are three kinds of reduction: beta-reduction ('betaReduce'),
|
||||
-- which defines how applications interact with lambda abstractions;
|
||||
-- eta-reduction ('etaReduce'), which describes how lambda abstractions interact with applications;
|
||||
-- and a new form, which I call scope-reduction ('scopeReduce'),
|
||||
-- which describes how 'Drop' scope delimiters propogate through expressions.
|
||||
--
|
||||
-- This function takes an expression and either reduces it,
|
||||
-- or, if there is no applicable reduction rule, returns nothing.
|
||||
-- The lack of an applicable reduction rule does not necessarily mean
|
||||
-- that an expression is irreducible: see 'evaluate' for more information.
|
||||
reduce :: Expression n -> Maybe (Expression n)
|
||||
-- Note: there are no expressions which are reducible in multiple ways.
|
||||
-- Only one of these cases can apply at once.
|
||||
reduce expr = scopeReduce expr <|> substitute expr <|> betaReduce expr <|> etaReduce expr
|
||||
|
||||
-- | A subexpression to which a reduction step may be applied is called a "redex",
|
||||
-- short for "reducible expression".
|
||||
isRedex :: Expression n -> Bool
|
||||
isRedex expr = isScopeRedex expr || isBetaRedex expr || isEtaRedex expr
|
||||
|
||||
-- | Beta reduction describes how functions behave when applied to arguments.
|
||||
-- To reduce a function application, you simply 'substitute` the parameter into the function body.
|
||||
--
|
||||
-- Beta reduction is the fundamental computation step of the lambda calculus.
|
||||
-- Only this rule is necessary for the lambda calculus to be turing-complete;
|
||||
-- the other reductions merely define *equivalences* between expressions,
|
||||
-- so that every expression has a canonical form.
|
||||
betaReduce :: Expression n -> Maybe (Expression n)
|
||||
betaReduce (Application (Abstraction fe) xe) = Just $ Substitution SZ xe fe
|
||||
-- (^) Aside: 'Application' represents function application in the lambda calculus.
|
||||
-- Haskell convention would be to name the function `f` and the argument `x`,
|
||||
-- but that often collides with Haskell functions and arguments,
|
||||
-- so instead I will be calling them `fe` and `xe`,
|
||||
-- where the `e` stands for "expression".
|
||||
betaReduce _ = Nothing
|
||||
|
||||
-- TODO: Document this.
|
||||
substitute :: Expression n -> Maybe (Expression n)
|
||||
substitute (Substitution SZ x Variable) = Just x
|
||||
substitute (Substitution (SS _) _ Variable) = Just Variable
|
||||
substitute (Substitution SZ x (Drop body)) = Just body
|
||||
substitute (Substitution (SS n) x (Drop body)) = Just $ Drop $ Substitution n x body
|
||||
substitute (Substitution n x (Application fe xe)) = Just $ Application (Substitution n x fe) (Substitution n x xe)
|
||||
substitute (Substitution n x (Abstraction body)) = Just $ Abstraction $ Substitution (SS n) x body
|
||||
substitute _ = Nothing
|
||||
|
||||
-- | A predicate determining whether a subexpression would allow a beta-reduction step.
|
||||
isBetaRedex :: Expression n -> Bool
|
||||
isBetaRedex (Application (Abstraction _) _) = True
|
||||
isBetaRedex _ = False
|
||||
|
||||
-- | For any expression `f`, `f` is equivalent to `\x. ?f x`, a property called "eta-equivalence".
|
||||
-- The conversion between these two forms is called "eta-conversion",
|
||||
-- with the conversion from `f` to `\x. ?f x` being called "eta-expansion",
|
||||
-- and its inverse (from `\x. ?f x` to `f`) being called "eta-reduction".
|
||||
--
|
||||
-- This rule is not necessary for the lambda calculus to express computation;
|
||||
-- that's the purpose of 'betaReduce'; rather, it expresses the idea of "extensionality",
|
||||
-- which in general describes the principles that judge objects to be equal
|
||||
-- if they have the same external properties
|
||||
-- (from within the context of the logical system, i.e. without regard to representation).
|
||||
-- In the context of functions, this would mean that two functions are equal
|
||||
-- if and only if they give the same result for all arguments.
|
||||
etaReduce :: Expression n -> Maybe (Expression n)
|
||||
etaReduce (Abstraction (Application (Drop fe) Variable)) = Just fe
|
||||
etaReduce _ = Nothing
|
||||
|
||||
-- | A predicate determining whether a subexpression would allow an eta-reduction step.
|
||||
isEtaRedex :: Expression n -> Bool
|
||||
isEtaRedex (Abstraction (Application (Drop _) Variable )) = True
|
||||
isEtaRedex _ = False
|
||||
|
||||
-- | Eta-expansion, the inverse of 'etaReduce'.
|
||||
etaExpand :: Expression n -> Expression n
|
||||
etaExpand fe = Abstraction $ Application (Drop fe) Variable
|
||||
|
||||
-- TODO: Scope conversion isn't a real conversion relationship!
|
||||
-- 'scopeExpand' can only be applied a finite number of times.
|
||||
-- That doesn't break the code, but I don't want to misrepresent it.
|
||||
-- 'scopeExpand' is only the *left* inverse of 'scopeReduce',
|
||||
-- not the inverse overall.
|
||||
--
|
||||
-- Alternatively, 'scopeExpand' could be defined on expressions with no sub-expressions.
|
||||
-- That would make sense, but then 'scopeReduce' would also have to be defined like that,
|
||||
-- which would make every reduction valid as well, meaning we can't use it in the same way
|
||||
-- we use the other reduction, because it always succeeds, and thus every expression
|
||||
-- could be considered reducible.
|
||||
--
|
||||
-- Perhaps delimiting scope should be external to the notion of an expression,
|
||||
-- like how Thyer represented it in the "Lazy Specialization" paper
|
||||
-- (http://thyer.name/phd-thesis/thesis-thyer.pdf).
|
||||
--
|
||||
-- In addition, it really doesn't fit in with the current scheme of reductions.
|
||||
-- It doesn't apply to any particular constructor/eliminator relationship,
|
||||
-- instead being this bizarre syntactical fragment instead of a real expression.
|
||||
-- After all, I could have also chosen to represent the calculus
|
||||
-- so that variables are parameterized by `Fin n` instead of being wrapped in stacks of 'Drop'.
|
||||
--
|
||||
-- I think this problem will work itself out as I work further on evaluation strategies
|
||||
-- and alternative representations, but for now, it'll do.
|
||||
-- | Scope-conversion describes how 'Drop'-delimited scopes propgate through expressions.
|
||||
-- It expresses the idea that a variable is used in an expression
|
||||
-- if and only if it is used in at least one of its sub-expressions.
|
||||
--
|
||||
-- Similarly to 'etaReduce', there is also define an inverse function, 'scopeExpand'.
|
||||
scopeReduce :: Expression n -> Maybe (Expression n)
|
||||
scopeReduce (Application (Drop fe) (Drop xe)) = Just $ Drop $ Application fe xe
|
||||
-- TODO: I feel like there's a more elegant way to represent this.
|
||||
-- It feels like `Abstraction (Drop body)` should be its own atomic unit.
|
||||
-- Maybe I could consider a combinator-based representation,
|
||||
-- where `Abstraction (Drop body)` is just the `K` combinator `K body`?
|
||||
scopeReduce (Abstraction (Drop (Drop body))) = Just $ Drop $ Abstraction $ Drop body
|
||||
scopeReduce _ = Nothing
|
||||
|
||||
-- | A predicate determining whether a subexpression would allow a scope-reduction step.
|
||||
isScopeRedex :: Expression n -> Bool
|
||||
isScopeRedex (Application (Drop _) (Drop _)) = True
|
||||
isScopeRedex (Abstraction (Drop (Drop _))) = True
|
||||
isScopeRedex _ = False
|
||||
|
||||
-- | Scope-expansion, the left inverse of 'scopeReduce'.
|
||||
scopeExpand :: Expression n -> Maybe (Expression n)
|
||||
scopeExpand (Drop (Application fe xe)) = Just $ Application (Drop fe) (Drop xe)
|
||||
scopeExpand (Drop (Abstraction (Drop body))) = Just $ Abstraction $ Drop $ Drop body
|
||||
scopeExpand _ = Nothing
|
||||
|
||||
-- | An expression is in "normal form" if it contains no redexes (see 'isRedex').
|
||||
isNormal :: Expression n -> Bool
|
||||
isNormal expr = not (isRedex expr) && case expr of
|
||||
-- In addition to this expression not being a redex,
|
||||
-- we must check that none of its subexpressions are redexes either.
|
||||
Application fe xe -> isNormal fe && isNormal xe
|
||||
Abstraction e -> isNormal e
|
||||
Drop e -> isNormal e
|
||||
_ -> True
|
||||
|
||||
-- TODO: Finish the below documentation on reduction strategies. I got bored.
|
||||
-- | Now that we have defined the ways in which an expression may be reduced ('reduce'),
|
||||
-- we need to define a "reduction strategy" to describe in what order we will apply reductions.
|
||||
-- Different reduction strategies have different performance characteristics,
|
||||
-- and even produce different results.
|
||||
--
|
||||
-- One of the most important distinctions between strategies is whether they are "normalizing".
|
||||
-- A normalising strategy will terminate if and only if
|
||||
-- the expression it is normalizing has a normal form.
|
||||
--
|
||||
-- I have chosen to use a normalizing reduction strategy.
|
||||
eval :: Expression n -> Expression n
|
||||
eval expr = case reduce innerReduced of
|
||||
Just e -> eval e
|
||||
-- The expression didn't make any progress,
|
||||
-- so we know that no further reductions can be applied here.
|
||||
-- It must be blocked on something.
|
||||
-- TODO: return why we stopped evaluating,
|
||||
-- so we can avoid redundantly re-evaluating stuff if nothing changed.
|
||||
Nothing -> innerReduced
|
||||
where innerReduced = case expr of
|
||||
-- TODO: Factor out this recursive case (from 'isNormal' too).
|
||||
Application fe xe -> Application (eval fe) (eval xe)
|
||||
Abstraction e -> Abstraction (eval e)
|
||||
Drop e -> Drop (eval e)
|
||||
x -> x
|
||||
@ -0,0 +1,137 @@
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
module LambdaCalculus.Expression where
|
||||
|
||||
import Data.List (elemIndex, find)
|
||||
import Data.Maybe (fromJust)
|
||||
import Data.HashSet (HashSet)
|
||||
import qualified Data.HashSet as HS
|
||||
import GHC.Generics (Generic)
|
||||
|
||||
data Expression
|
||||
= Variable String
|
||||
| Application Expression Expression
|
||||
| Abstraction String Expression
|
||||
deriving (Eq, Generic)
|
||||
|
||||
instance Show Expression where
|
||||
show (Variable var) = var
|
||||
show (Application ef ex) = "(" ++ show ef ++ " " ++ show ex ++ ")"
|
||||
show (Abstraction var body) = "(^" ++ var ++ "." ++ show body ++ ")"
|
||||
|
||||
-- | Free variables are variables which are present in an expression but not bound by any abstraction.
|
||||
freeVariables :: Expression -> HashSet String
|
||||
freeVariables (Variable variable) = HS.singleton variable
|
||||
freeVariables (Application ef ex) = freeVariables ef `HS.union` freeVariables ex
|
||||
freeVariables (Abstraction variable body) = HS.delete variable $ freeVariables body
|
||||
|
||||
-- | Return True if the given variable is free in the given expression.
|
||||
freeIn :: String -> Expression -> Bool
|
||||
freeIn var1 (Variable var2) = var1 == var2
|
||||
freeIn var (Application ef ex) = var `freeIn` ef && var `freeIn` ex
|
||||
freeIn var1 (Abstraction var2 body) = var1 == var2 || var1 `freeIn` body
|
||||
|
||||
-- | Bound variables are variables which are bound by any abstraction in an expression.
|
||||
boundVariables :: Expression -> HashSet String
|
||||
boundVariables (Variable _) = HS.empty
|
||||
boundVariables (Application ef ex) = boundVariables ef `HS.union` boundVariables ex
|
||||
boundVariables (Abstraction variable body) = HS.insert variable $ boundVariables body
|
||||
|
||||
-- | A closed expression is an expression with no free variables.
|
||||
-- Closed expressions are also known as combinators and are equivalent to terms in combinatory logic.
|
||||
closed :: Expression -> Bool
|
||||
closed = HS.null . freeVariables
|
||||
|
||||
-- | Alpha-equivalent terms differ only by the names of bound variables,
|
||||
-- i.e. one can be converted to the other using only alpha-conversion.
|
||||
alphaEquivalent :: Expression -> Expression -> Bool
|
||||
alphaEquivalent = alphaEquivalent' [] []
|
||||
where alphaEquivalent' :: [String] -> [String] -> Expression -> Expression -> Bool
|
||||
alphaEquivalent' ctx1 ctx2 (Variable v1) (Variable v2)
|
||||
-- Two variables are alpha-equivalent if they are bound in the same location.
|
||||
= bindingSite ctx1 v1 == bindingSite ctx2 v2
|
||||
alphaEquivalent' ctx1 ctx2 (Application ef1 ex1) (Application ef2 ex2)
|
||||
-- Two applications are alpha-equivalent if their components are alpha-equivalent.
|
||||
= alphaEquivalent' ctx1 ctx2 ef1 ef2
|
||||
&& alphaEquivalent' ctx1 ctx2 ex1 ex2
|
||||
alphaEquivalent' ctx1 ctx2 (Abstraction v1 b1) (Abstraction v2 b2)
|
||||
-- Two abstractions are alpha-equivalent if their bodies are alpha-equivalent.
|
||||
= alphaEquivalent' (v1 : ctx1) (v2 : ctx2) b1 b2
|
||||
|
||||
-- | The binding site of a variable is either the index of its binder
|
||||
-- or, if it is unbound, the name of the free variable.
|
||||
bindingSite :: [String] -> String -> Either String Int
|
||||
bindingSite ctx var = maybeToRight var $ var `elemIndex` ctx
|
||||
where maybeToRight :: b -> Maybe a -> Either b a
|
||||
maybeToRight default_ = maybe (Left default_) Right
|
||||
|
||||
-- | Substitution is the process of replacing all free occurrences of a variable in one expression with another expression.
|
||||
substitute :: String -> Expression -> Expression -> Expression
|
||||
substitute var1 value unmodified@(Variable var2)
|
||||
| var1 == var2 = value
|
||||
| otherwise = unmodified
|
||||
substitute var value (Application ef ex)
|
||||
= Application (substitute var value ef) (substitute var value ex)
|
||||
substitute var1 value unmodified@(Abstraction var2 body)
|
||||
| var1 == var2 = unmodified
|
||||
| otherwise = Abstraction var2' $ substitute var1 value $ alphaConvert var2 var2' body
|
||||
where var2' = escapeName (freeVariables value) var2
|
||||
alphaConvert oldName newName expr = substitute oldName (Variable newName) expr
|
||||
-- | Generate a new name which isn't present in the set, based on the old name.
|
||||
escapeName env name = fromJust $ find (not . free) names
|
||||
where names = name : map ('\'' :) names
|
||||
free = (`HS.member` env)
|
||||
|
||||
-- | Returns True if the top-level expression is reducible by beta-reduction.
|
||||
betaRedex :: Expression -> Bool
|
||||
betaRedex (Application (Abstraction _ _) _) = True
|
||||
betaRedex _ = False
|
||||
|
||||
-- | Returns True if the top-level expression is reducible by eta-reduction.
|
||||
etaRedex :: Expression -> Bool
|
||||
etaRedex (Abstraction var1 (Application ef (Variable var2)))
|
||||
= var1 /= var2 || var1 `freeIn` ef
|
||||
etaRedex _ = False
|
||||
|
||||
-- | In an expression in normal form, all reductions that can be applied have been applied.
|
||||
-- This is the result of applying eager evaluation.
|
||||
normal :: Expression -> Bool
|
||||
-- The expression is beta-reducible.
|
||||
normal (Application (Abstraction _ _) _) = False
|
||||
-- The expression is eta-reducible.
|
||||
normal (Abstraction var1 (Application fe (Variable var2)))
|
||||
= var1 /= var2 || var1 `freeIn` fe
|
||||
normal (Application ef ex) = normal ef && normal ex
|
||||
normal _ = True
|
||||
|
||||
-- | In an expression in weak head normal form, reductions to the function have been applied,
|
||||
-- but not all reductions to the parameter have been applied.
|
||||
-- This is the result of applying lazy evaluation.
|
||||
whnf :: Expression -> Bool
|
||||
whnf (Application (Abstraction _ _) _) = False
|
||||
whnf (Abstraction var1 (Application fe (Variable var2)))
|
||||
= var1 /= var2 || var1 `freeIn` fe
|
||||
whnf (Application ef _) = whnf ef
|
||||
|
||||
eval :: (Expression -> Expression) -> Expression -> Expression
|
||||
eval strategy = eval'
|
||||
where eval' :: Expression -> Expression
|
||||
eval' (Application ef ex) =
|
||||
case ef' of
|
||||
-- Beta-reduction
|
||||
Abstraction var body -> eval' $ substitute var ex' body
|
||||
_ -> Application ef' ex'
|
||||
where ef' = eval' ef
|
||||
ex' = strategy ex
|
||||
eval' unmodified@(Abstraction var1 (Application ef (Variable var2)))
|
||||
-- Eta-reduction
|
||||
| var1 == var2 && not (var1 `freeIn` ef) = eval' ef
|
||||
| otherwise = unmodified
|
||||
eval' x = x
|
||||
|
||||
-- | Reduce an expression to normal form.
|
||||
eagerEval :: Expression -> Expression
|
||||
eagerEval = eval eagerEval
|
||||
|
||||
-- | Reduce an expression to weak head normal form.
|
||||
lazyEval :: Expression -> Expression
|
||||
lazyEval = eval id
|
||||
@ -1,79 +1,37 @@
|
||||
module LambdaCalculus.Parser (parse) where
|
||||
module LambdaCalculus.Parser (parseExpression) where
|
||||
|
||||
import Control.Applicative (liftA2)
|
||||
import Control.Applicative ((*>))
|
||||
import Control.Monad (void)
|
||||
import Text.Parsec hiding (parse)
|
||||
import qualified Text.Parsec as Parsec
|
||||
import Text.Parsec.String (Parser)
|
||||
import LambdaCalculus.Representation.AbstractSyntax
|
||||
import LambdaCalculus.Expression (Expression (Variable, Application, Abstraction))
|
||||
import Text.Parsec hiding (spaces)
|
||||
import Text.Parsec.String
|
||||
|
||||
-- | Parse a keyword, unambiguously not a variable name.
|
||||
keyword :: String -> Parser ()
|
||||
keyword kwd = try $ do
|
||||
void $ string kwd
|
||||
-- TODO: rephrase this in terms of `extension`
|
||||
notFollowedBy alphaNum
|
||||
spaces :: Parser ()
|
||||
spaces = void $ many1 space
|
||||
|
||||
-- | The extension of a variable name.
|
||||
-- The first letter of a variable name must be a letter,
|
||||
-- but the rest of the variable name may be more general.
|
||||
extension :: Parser String
|
||||
extension = many alphaNum
|
||||
variableName :: Parser String
|
||||
variableName = many1 letter
|
||||
|
||||
-- | A variable name, e.g. `x`, `foo`, `f2`, `fooBar27`.
|
||||
name :: Parser String
|
||||
name = do
|
||||
notFollowedBy anyKeyword
|
||||
liftA2 (:) letter extension
|
||||
where
|
||||
anyKeyword = choice $ map keyword keywords
|
||||
where
|
||||
-- | Keywords that are forbidden from use as variable names.
|
||||
keywords = ["let", "in"]
|
||||
|
||||
-- | A variable expression.
|
||||
variable :: Parser Expression
|
||||
variable = Variable <$> name
|
||||
variable = Variable <$> variableName
|
||||
|
||||
-- | A lambda abstraction.
|
||||
abstraction :: Parser Expression
|
||||
abstraction = do
|
||||
char 'λ' <|> char '\\' ; spaces
|
||||
variables <- variableList ; spaces
|
||||
char '.' ; spaces
|
||||
body <- expression
|
||||
return $ Abstraction variables body
|
||||
where variableList :: Parser [String]
|
||||
variableList = name `sepBy` spaces
|
||||
|
||||
-- | A function application.
|
||||
application :: Parser Expression
|
||||
application = Application <$> applicationTerm `sepEndBy` spaces
|
||||
where
|
||||
-- | An application term is any expression which consumes input,
|
||||
-- i.e. anything other than an ungrouped application.
|
||||
applicationTerm :: Parser Expression
|
||||
applicationTerm = let_ <|> variable <|> abstraction <|> grouping
|
||||
where
|
||||
-- | An expression grouped by parentheses.
|
||||
grouping :: Parser Expression
|
||||
grouping = between (char '(' >> spaces) (spaces >> char ')') expression
|
||||
application = foldl1 Application <$> sepBy1 applicationTerm spaces
|
||||
where applicationTerm :: Parser Expression
|
||||
applicationTerm = variable <|> abstraction <|> grouping
|
||||
where grouping :: Parser Expression
|
||||
grouping = between (char '(') (char ')') expression
|
||||
|
||||
-- | A `let` expression.
|
||||
let_ :: Parser Expression
|
||||
let_ = do
|
||||
keyword "let" ; spaces
|
||||
variable <- name ; spaces
|
||||
char '=' ; spaces
|
||||
value <- expression ; spaces
|
||||
string "in" ; spaces
|
||||
abstraction :: Parser Expression
|
||||
abstraction = do
|
||||
char '^'
|
||||
names <- sepBy1 variableName spaces
|
||||
char '.'
|
||||
body <- expression
|
||||
return $ Let variable value body
|
||||
pure $ foldr Abstraction body names
|
||||
|
||||
-- | Any expression.
|
||||
expression :: Parser Expression
|
||||
expression = application
|
||||
expression = abstraction <|> application <|> variable
|
||||
|
||||
-- | Parse a lambda calculus expression.
|
||||
parse :: SourceName -> String -> Either ParseError Expression
|
||||
parse = Parsec.parse (expression <* eof)
|
||||
parseExpression :: String -> Either ParseError Expression
|
||||
parseExpression = parse (expression <* eof) "input"
|
||||
|
||||
@ -1,30 +0,0 @@
|
||||
module LambdaCalculus.Representation where
|
||||
|
||||
import Data.Functor.Foldable (cata)
|
||||
import Data.HashSet (HashSet, singleton, union, delete)
|
||||
import LambdaCalculus.Representation.Standard
|
||||
|
||||
-- | `expr` is a representation of a /closed/ lambda calculus expression.
|
||||
class IsExpr expr where
|
||||
-- | Convert an expression to the standard representation.
|
||||
toStandard :: expr -> Expression
|
||||
|
||||
-- | Convert an expression from the standard representation.
|
||||
fromStandard :: Expression -> expr
|
||||
|
||||
-- | Convert an expression from one representation to another.
|
||||
convert :: IsExpr repr => expr -> repr
|
||||
convert = fromStandard . toStandard
|
||||
|
||||
-- | Retrieve the free variables in an expression.
|
||||
freeVariables :: expr -> HashSet String
|
||||
freeVariables = freeVariables . toStandard
|
||||
|
||||
instance IsExpr Expression where
|
||||
toStandard = id
|
||||
fromStandard = id
|
||||
convert = fromStandard
|
||||
freeVariables = cata \case
|
||||
VariableF name -> singleton name
|
||||
AbstractionF name body -> name `delete` body
|
||||
ApplicationF fe xe -> fe `union` xe
|
||||
@ -1,76 +0,0 @@
|
||||
module LambdaCalculus.Representation.AbstractSyntax where
|
||||
|
||||
import Control.Comonad.Cofree (Cofree ((:<)))
|
||||
import Data.Functor.Foldable (cata, histo)
|
||||
import Data.Functor.Foldable.TH (makeBaseFunctor)
|
||||
import Data.List (foldl1')
|
||||
import LambdaCalculus.Combinators (i)
|
||||
import LambdaCalculus.Representation
|
||||
import qualified LambdaCalculus.Representation.Standard as Std
|
||||
|
||||
data Expression = Variable String
|
||||
| Abstraction [String] Expression
|
||||
| Application [Expression]
|
||||
-- | `let name = value in body`
|
||||
| Let String Expression Expression
|
||||
|
||||
makeBaseFunctor ''Expression
|
||||
|
||||
instance Show Expression where
|
||||
show = histo \case
|
||||
VariableF name -> name
|
||||
AbstractionF names (body :< _) -> "λ" ++ unwords names ++ ". " ++ body
|
||||
-- TODO: this is a weird implementation of re-grouping variables,
|
||||
-- to the degree that explicit recursion would probably be more clear.
|
||||
-- Clean this up!
|
||||
ApplicationF exprs -> unwords $ mapExceptLast regroup regroupApplication exprs
|
||||
LetF name (value :< _) (body :< _)
|
||||
-> "let " ++ name ++ " = " ++ value ++ " in " ++ body
|
||||
where regroup (expr :< AbstractionF _ _) = group expr
|
||||
regroup (expr :< LetF _ _ _) = group expr
|
||||
regroup expr = regroupApplication expr
|
||||
|
||||
regroupApplication (expr :< ApplicationF _) = group expr
|
||||
regroupApplication (expr :< _) = expr
|
||||
|
||||
group str = "(" ++ str ++ ")"
|
||||
|
||||
-- | Map the first function to all but the last element of the list,
|
||||
-- and the last function to only the last element.
|
||||
mapExceptLast :: (a -> b) -> (a -> b) -> [a] -> [b]
|
||||
-- TODO: express this as a paramorphism
|
||||
mapExceptLast _ _ [] = []
|
||||
mapExceptLast _ fLast [x] = [fLast x]
|
||||
mapExceptLast f fLast (x:xs) = f x : mapExceptLast f fLast xs
|
||||
|
||||
instance IsExpr Expression where
|
||||
toStandard = cata \case
|
||||
VariableF name -> Std.Variable name
|
||||
-- We could technically just use `foldl' Std.Application i exprs`,
|
||||
-- since that's the justification for allowing non-binary applications in the first place,
|
||||
-- but we want expressions using only binary applications
|
||||
-- to still generate the same expression,
|
||||
-- not just beta-equivalent expressions.
|
||||
ApplicationF [] -> i
|
||||
ApplicationF [expr] -> expr
|
||||
ApplicationF exprs -> foldl1' Std.Application exprs
|
||||
AbstractionF names body -> foldr Std.Abstraction body names
|
||||
LetF name value body -> Std.Application (Std.Abstraction name body) value
|
||||
|
||||
-- Again with the intent of generating the canonical form for this representation,
|
||||
-- we want to convert all left-nested applications into a list application;
|
||||
-- similarly, we convert nested abstractions into a list of names,
|
||||
-- and abstractions into `let`s when applicable.
|
||||
fromStandard = histo \case
|
||||
Std.VariableF name -> Variable name
|
||||
-- `(\x. e) N` --> `let x = N in e`.
|
||||
Std.ApplicationF (_ :< Std.AbstractionF name (body :< _)) (value :< _)
|
||||
-> Let name value body
|
||||
Std.ApplicationF (Application exprs :< _) (xe :< _)
|
||||
-> Application $ exprs ++ [xe]
|
||||
Std.ApplicationF (fe :< _) (xe :< _)
|
||||
-> Application [fe, xe]
|
||||
Std.AbstractionF name (Abstraction names body :< _)
|
||||
-> Abstraction (name : names) body
|
||||
Std.AbstractionF name (body :< _)
|
||||
-> Abstraction [name] body
|
||||
@ -1,74 +0,0 @@
|
||||
module LambdaCalculus.Representation.Dependent.ReverseDeBruijn where
|
||||
|
||||
import Control.Monad.Reader (Reader, runReader, withReader, asks)
|
||||
import Data.Type.Equality ((:~:)(Refl))
|
||||
import Data.Type.Nat
|
||||
import Data.Vec
|
||||
import LambdaCalculus.Representation
|
||||
import qualified LambdaCalculus.Representation.Standard as Std
|
||||
|
||||
-- | Expressions are parametrized by the depth of the variable bindings they may access.
|
||||
-- An expression in which no variables are bound (a closed expression) is represented by `Expression 'Z`.
|
||||
data Expression :: Nat -> * where
|
||||
-- | The body of a lambda abstraction may reference all of the variables
|
||||
-- bound in its parent, in addition to a new variable bound by the abstraction.
|
||||
Abstraction :: Expression ('S n) -> Expression n
|
||||
-- | On the other hand, any sub-expression may choose to simply ignore
|
||||
-- the variable bound by the lambda expression,
|
||||
-- only referencing the variables bound in its parent instead.
|
||||
--
|
||||
-- For example, in the constant function `\x. \y. x`,
|
||||
-- although the innermost expression *may* access the innermost binding (`y`),
|
||||
-- it instead only accesses the outer one, `x`.
|
||||
-- Thus the body of the expression would be `Drop Variable`.
|
||||
--
|
||||
-- Given the lack of any convention for how to write 'Drop',
|
||||
-- I have chosen to write it as `?x` where `x` is the body of the drop.
|
||||
Drop :: Expression n -> Expression ('S n)
|
||||
-- | For this reason (see 'Drop'),
|
||||
-- variables only need to access the innermost accessible binding.
|
||||
-- To access outer bindings, you must first 'Drop' all of the bindings
|
||||
-- in between the variable and the desired binding to access.
|
||||
Variable :: Expression ('S n)
|
||||
-- | Function application. The left side is the function, and the right side is the argument.
|
||||
Application :: Expression n -> Expression n -> Expression n
|
||||
-- | A free expression is a symbolic placeholder which reduces to itself.
|
||||
Free :: String -> Expression 'Z
|
||||
Substitution :: SNat n -> Expression m -> Expression ('S (Plus n m)) -> Expression (Plus n m)
|
||||
|
||||
instance SNatI n => Show (Expression n) where
|
||||
show expr = show' snat expr
|
||||
where show' :: SNat n -> Expression n -> String
|
||||
show' (SS n) Variable = show n
|
||||
show' SZ (Free name) = name
|
||||
show' (SS n) (Drop body) = '?' : show' n body
|
||||
show' n (Abstraction body) = "(\\" ++ show n ++ " " ++ show' (SS n) body ++ ")"
|
||||
show' n (Application fe xe) = "(" ++ show' n fe ++ " " ++ show' n xe ++ ")"
|
||||
|
||||
instance IsExpr (Expression 'Z) where
|
||||
fromStandard expr = runReader (fromStandard' expr) VNil
|
||||
where fromStandard' :: SNatI n => Std.Expression -> Reader (Vec n String) (Expression n)
|
||||
-- TODO: This code is absolutely atrocious.
|
||||
-- It is in dire need of cleanup.
|
||||
fromStandard' (Std.Variable name) = asks $ makeVar snat SZ
|
||||
where makeVar :: SNat n -> SNat m -> Vec n String -> Expression (Plus m n)
|
||||
makeVar SZ m VNil = dropEm m $ Free name
|
||||
makeVar (SS n) m (var ::: bound) = case plusSuc m n of
|
||||
Refl
|
||||
| name == var -> dropEm2 n m
|
||||
| otherwise -> makeVar n (SS m) bound
|
||||
|
||||
dropEm :: SNat m -> Expression n -> Expression (Plus m n)
|
||||
dropEm SZ e = e
|
||||
dropEm (SS n) e = Drop $ dropEm n e
|
||||
|
||||
dropEm2 :: SNat n -> SNat m -> Expression ('S (Plus m n))
|
||||
dropEm2 _ SZ = Variable
|
||||
dropEm2 n (SS m) = Drop $ dropEm2 n m
|
||||
fromStandard' (Std.Abstraction name body)
|
||||
= fmap Abstraction $ withReader (name :::) $ fromStandard' body
|
||||
fromStandard' (Std.Application fe xe)
|
||||
= Application <$> fromStandard' fe <*> fromStandard' xe
|
||||
|
||||
-- TODO: Implement this. Important!
|
||||
toStandard expr = undefined
|
||||
@ -1,18 +0,0 @@
|
||||
module LambdaCalculus.Representation.Standard where
|
||||
|
||||
import Data.Functor.Foldable (cata)
|
||||
import Data.Functor.Foldable.TH (makeBaseFunctor)
|
||||
|
||||
data Expression = Variable String
|
||||
| Abstraction String Expression
|
||||
| Application Expression Expression
|
||||
|
||||
makeBaseFunctor ''Expression
|
||||
|
||||
instance Show Expression where
|
||||
-- For a more sophisticated printing mechanism,
|
||||
-- consider converting to 'LambdaCalculus.Representation.AbstractSyntax.Expression' first.
|
||||
show = cata \case
|
||||
VariableF name -> name
|
||||
AbstractionF name body -> "(λ" ++ name ++ ". " ++ body ++ ")"
|
||||
ApplicationF fe xe -> "(" ++ fe ++ " " ++ xe ++ ")"
|
||||
@ -0,0 +1,58 @@
|
||||
import Data.Char (isAlpha)
|
||||
import Generic.Random (genericArbitraryRec, uniform)
|
||||
import LambdaCalculus.Expression
|
||||
import LambdaCalculus.Parser
|
||||
import Test.QuickCheck
|
||||
import Test.Tasty
|
||||
import Test.Tasty.HUnit
|
||||
import Test.Tasty.QuickCheck
|
||||
|
||||
instance Arbitrary Expression where
|
||||
arbitrary = genericArbitraryRec uniform
|
||||
|
||||
dfi :: Expression
|
||||
dfi = Application d (Application f i)
|
||||
where d = Abstraction "x" $ Application (Variable "x") (Variable "x")
|
||||
f = Abstraction "f" $ Application (Variable "f") (Application (Variable "f") (Variable "y"))
|
||||
i = Abstraction "x" $ Variable "x"
|
||||
|
||||
ttttt :: Expression
|
||||
ttttt = Application (Application (Application f t) (Abstraction "x" (Variable "x"))) (Variable "y")
|
||||
where t = Abstraction "f" $ Abstraction "x" $
|
||||
Application (Variable "f") (Application (Variable "f") (Variable "x"))
|
||||
f = Abstraction "T" $ Abstraction "f" $ Abstraction "x" $
|
||||
Application (Application
|
||||
(Application (Variable "T")
|
||||
(Application (Variable "T")
|
||||
(Application (Variable "T")
|
||||
(Application (Variable "T")
|
||||
(Variable "T")))))
|
||||
(Variable "f"))
|
||||
(Variable "x")
|
||||
|
||||
prop_parseExpression_inverse :: Expression -> Bool
|
||||
prop_parseExpression_inverse expr' = Right expr == parseExpression (show expr)
|
||||
where expr = legalizeVariables expr'
|
||||
legalizeVariables (Variable var) = Variable $ legalVar var
|
||||
legalizeVariables (Application ef ex) = Application (legalizeVariables ef) (legalizeVariables ex)
|
||||
legalizeVariables (Abstraction var body) = Abstraction (legalVar var) $ legalizeVariables body
|
||||
legalVar var = 'v' : filter isAlpha var
|
||||
|
||||
|
||||
main :: IO ()
|
||||
main = defaultMain $
|
||||
testGroup "Tests"
|
||||
[ testGroup "Evaluator tests"
|
||||
[ testCase "DFI" $ eagerEval dfi @?= Application (Variable "y") (Variable "y")
|
||||
, testCase "ttttt" $ eagerEval ttttt @?= Variable "y"
|
||||
]
|
||||
, testGroup "Parser tests"
|
||||
[ testGroup "Unit tests"
|
||||
[ testCase "identity" $ parseExpression "^x.x" @?= Right (Abstraction "x" $ Variable "x")
|
||||
, testCase "application shorthand" $ parseExpression "a b c d" @?= Right (Application (Application (Application (Variable "a") (Variable "b")) (Variable "c")) (Variable "d"))
|
||||
, testCase "ttttt" $ parseExpression "(^T f x.(T (T (T (T T)))) f x) (^f x.f (f x)) (^x.x) y"
|
||||
@?= Right ttttt
|
||||
]
|
||||
, testProperty "parseExpression is the left inverse of show" prop_parseExpression_inverse
|
||||
]
|
||||
]
|
||||
Loading…
Reference in New Issue