Portability | portable |
---|---|
Stability | experimental |
Maintainer | Edward Kmett <ekmett@gmail.com> |
Safe Haskell | Safe-Inferred |
We represent the target language itself as an ideal monad supplied by the
user, and provide a Scope
monad transformer for introducing bound
variables in user supplied terms. Users supply a Monad
and Traversable
instance, and we traverse to find free variables, and use the Monad
to
perform substitution that avoids bound variables.
An untyped lambda calculus:
{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
import Bound
import Control.Applicative
import Control.Monad (ap
)
import Prelude.Extras
import Data.Foldable
import Data.Traverable
infixl 9 :@ data Exp a = V a | Exp a :@ Exp a | Lam (Scope
() Exp a) deriving (Eq
,Ord
,Show
,Read
,Functor
,Foldable
,Traversable
)
instanceEq1
Exp where (==#
) = (==
) instanceOrd1
Exp wherecompare1
=compare
instanceShow1
Exp whereshowsPrec1
=showsPrec
instanceRead1
Exp wherereadsPrec1
=readsPrec
instanceApplicative
Exp wherepure
= V; (<*>
) =ap
instanceMonad
Exp wherereturn
= V V a>>=
f = f a (x :@ y)>>=
f = (x>>=
f) :@ (y >>= f) Lam e>>=
f = Lam (e>>>=
f)
lam ::Eq
a => a ->Exp
a ->Exp
a lam v b = Lam (abstract1
v b)
whnf ::Exp
a ->Exp
a whnf (f :@ a) = case whnf f of Lam b -> whnf (instantiate1
a b) f' -> f' :@ a whnf e = e
More exotic combinators for manipulating a Scope
can be imported from
Bound.Scope.
You can also retain names in your bound variables by using Name
and the related combinators from Bound.Name. They are not re-exported
from this module by default.
- substitute :: (Monad f, Eq a) => a -> f a -> f a -> f a
- isClosed :: Foldable f => f a -> Bool
- closed :: Traversable f => f a -> Maybe (f b)
- newtype Scope b f a = Scope {}
- abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a
- abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a
- instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a
- instantiate1 :: Monad f => f a -> Scope n f a -> f a
- class Bound t where
- (=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f c
- data Var b a
- fromScope :: Monad f => Scope b f a -> f (Var b a)
- toScope :: Monad f => f (Var b a) -> Scope b f a
Manipulating user terms
substitute :: (Monad f, Eq a) => a -> f a -> f a -> f aSource
replaces the free variable substitute
a p wa
with p
in w
.
>>>
substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]
["goodnight","Gracie","!!!"]
isClosed :: Foldable f => f a -> BoolSource
A closed term has no free variables.
>>>
isClosed []
True
>>>
isClosed [1,2,3]
False
closed :: Traversable f => f a -> Maybe (f b)Source
If a term has no free variables, you can freely change the type of free variables it is parameterized on.
>>>
closed [12]
Nothing
>>>
closed ""
Just []
>>>
:t closed ""
closed "" :: Maybe [b]
Scopes introduce bound variables
is an Scope
b f af
expression with bound variables in b
,
and free variables in a
We store bound variables as their generalized de Bruijn
representation in that we're allowed to lift
(using F
) an entire
tree rather than only succ individual variables, but we're still
only allowed to do so once per Scope
. Weakening trees permits
O(1) weakening and permits more sharing opportunities. Here the
deBruijn 0 is represented by the B
constructor of Var
, while the
de Bruijn succ
(which may be applied to an entire tree!) is handled
by F
.
NB: equality and comparison quotient out the distinct F
placements
allowed by the generalized de Bruijn representation and return the
same result as a traditional de Bruijn representation would.
Logically you can think of this as if the shape were the traditional
f (Var b a)
, but the extra f a
inside permits us a cheaper lift
.
MonadTrans (Scope b) | |
Bound (Scope b) | |
Monad f => Monad (Scope b f) | The monad permits substitution on free variables, while preserving bound variables |
Functor f => Functor (Scope b f) | |
Foldable f => Foldable (Scope b f) |
|
(Functor (Scope b f), Foldable (Scope b f), Traversable f) => Traversable (Scope b f) | |
(Monad f, Eq b, Eq1 f) => Eq1 (Scope b f) | |
(Eq1 (Scope b f), Monad f, Ord b, Ord1 f) => Ord1 (Scope b f) | |
(Functor f, Show b, Show1 f) => Show1 (Scope b f) | |
(Functor f, Read b, Read1 f) => Read1 (Scope b f) | |
(Monad f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a) | |
(Eq (Scope b f a), Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a) | |
(Functor f, Read b, Read1 f, Read a) => Read (Scope b f a) | |
(Functor f, Show b, Show1 f, Show a) => Show (Scope b f a) |
Abstraction over bound variables
abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f aSource
Capture some free variables in an expression to yield
a Scope
with bound variables in b
>>>
:m + Data.List
>>>
abstract (`elemIndex` "bar") "barry"
Scope [B 0,B 1,B 2,B 2,F "y"]
abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f aSource
Abstract over a single variable
>>>
abstract1 'x' "xyz"
Scope [B (),F "y",F "z"]
Instantiation of bound variables
instantiate :: Monad f => (b -> f a) -> Scope b f a -> f aSource
Enter a scope, instantiating all bound variables
>>>
:m + Data.List
>>>
instantiate (\x -> [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry"
"abccy"
instantiate1 :: Monad f => f a -> Scope n f a -> f aSource
Enter a Scope
that binds one variable, instantiating it
>>>
instantiate1 "x" $ Scope [B (),F "y",F "z"]
"xyz"
Structures permitting substitution
Instances of Bound
may or may not be monad transformers.
If they are, then m
is required to hold, and is
in fact the default definition. If it is not a >>>=
f ≡ m >>=
lift
.
fMonadTrans
instance, then
you have greater flexibility in how to implement this class.
This is useful for types like expression lists, case alternatives, schemas, etc. that may not be expressions in their own right, but often contain expressions.
Conversion to Traditional de Bruijn
"I am not a number, I am a free monad!"
A
is a variable that may either be "bound" (Var
b aB
) or "free" (F
).
(It is also technically a free monad in the same near-trivial sense as
Either
.)
Typeable2 Var | |
Bitraversable Var | |
Bifunctor Var | |
Bifoldable Var | |
Eq2 Var | |
Ord2 Var | |
Show2 Var | |
Read2 Var | |
Monad (Var b) | |
Functor (Var b) | |
Functor (Var b) => Applicative (Var b) | |
Foldable (Var b) | |
(Functor (Var b), Foldable (Var b)) => Traversable (Var b) | |
Eq b => Eq1 (Var b) | |
(Eq1 (Var b), Ord b) => Ord1 (Var b) | |
Show b => Show1 (Var b) | |
Read b => Read1 (Var b) | |
(Eq b, Eq a) => Eq (Var b a) | |
(Typeable (Var b a), Data b, Data a) => Data (Var b a) | |
(Eq (Var b a), Ord b, Ord a) => Ord (Var b a) | |
(Read b, Read a) => Read (Var b a) | |
(Show b, Show a) => Show (Var b a) | |
Generic (Var b a) |