bound-2.0.6: Making de Bruijn Succ Less

Bound

Description

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, TemplateHaskell #-}
import Bound
import Control.Applicative
import Control.Monad (ap)
import Data.Functor.Classes
import Data.Foldable
import Data.Traversable
-- This is from deriving-compat package
import Data.Deriving (deriveEq1, deriveOrd1, deriveRead1, deriveShow1)

infixl 9 :@
data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
deriving (Functor,Foldable,Traversable)

instance Applicative Exp where pure = V; (<*>) = ap
instance Monad Exp where
return = V
V a      >>= f = f a
(x :@ y) >>= f = (x >>= f) :@ (y >>= f)
Lam e    >>= f = Lam (e >>>= f)


## Abstraction over bound variables

abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a Source #

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 a Source #

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 a Source #

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 a Source # Enter a Scope that binds one variable, instantiating it >>> instantiate1 "x"$ Scope [B (),F "y",F "z"]
"xyz"


# Structures permitting substitution

class Bound t where Source #

Instances of Bound generate left modules over monads.

This means they should satisfy the following laws:

m >>>= return ≡ m
m >>>= (λ x → k x >>= h) ≡ (m >>>= k) >>>= h


This guarantees that a typical Monad instance for an expression type where Bound instances appear will satisfy the Monad laws (see doc/BoundLaws.hs).

If instances of Bound are monad transformers, then m >>>= f ≡ m >>= lift . f implies the above laws, and is in fact the default definition.

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.

Note: Free isn't "really" a monad transformer, even if the kind matches. Therefore there isn't Bound Free instance.

Minimal complete definition

Nothing

Methods

(>>>=) :: Monad f => t f a -> (a -> f c) -> t f c infixl 1 Source #

Perform substitution

If t is an instance of MonadTrans and you are compiling on GHC >= 7.4, then this gets the default definition:

m >>>= f = m >>= lift . f

default (>>>=) :: (MonadTrans t, Monad f, Monad (t f)) => t f a -> (a -> f c) -> t f c Source #

#### Instances

Instances details

(=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f c infixr 1 Source #

A flipped version of (>>>=).

(=<<<) = flip (>>>=)

# Conversion to Traditional de Bruijn

data Var b a Source #

"I am not a number, I am a free monad!"

A Var b a is a variable that may either be "bound" (B) or "free" (F).

(It is also technically a free monad in the same near-trivial sense as Either.)

Constructors

 B b this is a bound variable F a this is a free variable

#### Instances

Instances details
 Source # Instance detailsDefined in Bound.Var Methodsbifold :: Monoid m => Var m m -> m #bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Var a b -> m #bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Var a b -> c #bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Var a b -> c # Source # Instance detailsDefined in Bound.Var Methodsbimap :: (a -> b) -> (c -> d) -> Var a c -> Var b d #first :: (a -> b) -> Var a c -> Var b c #second :: (b -> c) -> Var a b -> Var a c # Source # Instance detailsDefined in Bound.Var Methodsbitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Var a b -> f (Var c d) # Source # Instance detailsDefined in Bound.Var MethodsliftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> Var a c -> Var b d -> Bool # Source # Instance detailsDefined in Bound.Var MethodsliftCompare2 :: (a -> b -> Ordering) -> (c -> d -> Ordering) -> Var a c -> Var b d -> Ordering # Source # Instance detailsDefined in Bound.Var MethodsliftReadsPrec2 :: (Int -> ReadS a) -> ReadS [a] -> (Int -> ReadS b) -> ReadS [b] -> Int -> ReadS (Var a b) #liftReadList2 :: (Int -> ReadS a) -> ReadS [a] -> (Int -> ReadS b) -> ReadS [b] -> ReadS [Var a b] #liftReadPrec2 :: ReadPrec a -> ReadPrec [a] -> ReadPrec b -> ReadPrec [b] -> ReadPrec (Var a b) #liftReadListPrec2 :: ReadPrec a -> ReadPrec [a] -> ReadPrec b -> ReadPrec [b] -> ReadPrec [Var a b] # Source # Instance detailsDefined in Bound.Var MethodsliftShowsPrec2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> Int -> Var a b -> ShowS #liftShowList2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> [Var a b] -> ShowS # Source # Instance detailsDefined in Bound.Var MethodsserializeWith2 :: MonadPut m => (a -> m ()) -> (b -> m ()) -> Var a b -> m () #deserializeWith2 :: MonadGet m => m a -> m b -> m (Var a b) # Source # Instance detailsDefined in Bound.Var MethodsliftHashWithSalt2 :: (Int -> a -> Int) -> (Int -> b -> Int) -> Int -> Var a b -> Int # Generic1 (Var b :: Type -> Type) Source # Instance detailsDefined in Bound.Var Associated Typestype Rep1 (Var b) :: k -> Type # Methodsfrom1 :: forall (a :: k). Var b a -> Rep1 (Var b) a #to1 :: forall (a :: k). Rep1 (Var b) a -> Var b a # Foldable (Var b) Source # Instance detailsDefined in Bound.Var Methodsfold :: Monoid m => Var b m -> m #foldMap :: Monoid m => (a -> m) -> Var b a -> m #foldMap' :: Monoid m => (a -> m) -> Var b a -> m #foldr :: (a -> b0 -> b0) -> b0 -> Var b a -> b0 #foldr' :: (a -> b0 -> b0) -> b0 -> Var b a -> b0 #foldl :: (b0 -> a -> b0) -> b0 -> Var b a -> b0 #foldl' :: (b0 -> a -> b0) -> b0 -> Var b a -> b0 #foldr1 :: (a -> a -> a) -> Var b a -> a #foldl1 :: (a -> a -> a) -> Var b a -> a #toList :: Var b a -> [a] #null :: Var b a -> Bool #length :: Var b a -> Int #elem :: Eq a => a -> Var b a -> Bool #maximum :: Ord a => Var b a -> a #minimum :: Ord a => Var b a -> a #sum :: Num a => Var b a -> a #product :: Num a => Var b a -> a # Eq b => Eq1 (Var b) Source # Instance detailsDefined in Bound.Var MethodsliftEq :: (a -> b0 -> Bool) -> Var b a -> Var b b0 -> Bool # Ord b => Ord1 (Var b) Source # Instance detailsDefined in Bound.Var MethodsliftCompare :: (a -> b0 -> Ordering) -> Var b a -> Var b b0 -> Ordering # Read b => Read1 (Var b) Source # Instance detailsDefined in Bound.Var MethodsliftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Var b a) #liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [Var b a] #liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (Var b a) #liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [Var b a] # Show b => Show1 (Var b) Source # Instance detailsDefined in Bound.Var MethodsliftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Var b a -> ShowS #liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Var b a] -> ShowS # Source # Instance detailsDefined in Bound.Var Methodstraverse :: Applicative f => (a -> f b0) -> Var b a -> f (Var b b0) #sequenceA :: Applicative f => Var b (f a) -> f (Var b a) #mapM :: Monad m => (a -> m b0) -> Var b a -> m (Var b b0) #sequence :: Monad m => Var b (m a) -> m (Var b a) # Source # Instance detailsDefined in Bound.Var Methodspure :: a -> Var b a #(<*>) :: Var b (a -> b0) -> Var b a -> Var b b0 #liftA2 :: (a -> b0 -> c) -> Var b a -> Var b b0 -> Var b c #(*>) :: Var b a -> Var b b0 -> Var b b0 #(<*) :: Var b a -> Var b b0 -> Var b a # Functor (Var b) Source # Instance detailsDefined in Bound.Var Methodsfmap :: (a -> b0) -> Var b a -> Var b b0 #(<$) :: a -> Var b b0 -> Var b a # Monad (Var b) Source # Instance detailsDefined in Bound.Var Methods(>>=) :: Var b a -> (a -> Var b b0) -> Var b b0 #(>>) :: Var b a -> Var b b0 -> Var b b0 #return :: a -> Var b a # Serial b => Serial1 (Var b) Source # Instance detailsDefined in Bound.Var MethodsserializeWith :: MonadPut m => (a -> m ()) -> Var b a -> m () #deserializeWith :: MonadGet m => m a -> m (Var b a) # Hashable b => Hashable1 (Var b) Source # Instance detailsDefined in Bound.Var MethodsliftHashWithSalt :: (Int -> a -> Int) -> Int -> Var b a -> Int # (Data b, Data a) => Data (Var b a) Source # Instance detailsDefined in Bound.Var Methodsgfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> Var b a -> c (Var b a) #gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Var b a) #toConstr :: Var b a -> Constr #dataTypeOf :: Var b a -> DataType #dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Var b a)) #dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Var b a)) #gmapT :: (forall b0. Data b0 => b0 -> b0) -> Var b a -> Var b a #gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var b a -> r #gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var b a -> r #gmapQ :: (forall d. Data d => d -> u) -> Var b a -> [u] #gmapQi :: Int -> (forall d. Data d => d -> u) -> Var b a -> u #gmapM :: Monad m => (forall d. Data d => d -> m d) -> Var b a -> m (Var b a) #gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Var b a -> m (Var b a) #gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Var b a -> m (Var b a) # Generic (Var b a) Source # Instance detailsDefined in Bound.Var Associated Typestype Rep (Var b a) :: Type -> Type # Methodsfrom :: Var b a -> Rep (Var b a) x #to :: Rep (Var b a) x -> Var b a # (Read b, Read a) => Read (Var b a) Source # Instance detailsDefined in Bound.Var MethodsreadsPrec :: Int -> ReadS (Var b a) #readList :: ReadS [Var b a] #readPrec :: ReadPrec (Var b a) #readListPrec :: ReadPrec [Var b a] # (Show b, Show a) => Show (Var b a) Source # Instance detailsDefined in Bound.Var MethodsshowsPrec :: Int -> Var b a -> ShowS #show :: Var b a -> String #showList :: [Var b a] -> ShowS # (Binary b, Binary a) => Binary (Var b a) Source # Instance detailsDefined in Bound.Var Methodsput :: Var b a -> Put #get :: Get (Var b a) #putList :: [Var b a] -> Put # (Serial b, Serial a) => Serial (Var b a) Source # Instance detailsDefined in Bound.Var Methodsserialize :: MonadPut m => Var b a -> m () #deserialize :: MonadGet m => m (Var b a) # (Serialize b, Serialize a) => Serialize (Var b a) Source # Instance detailsDefined in Bound.Var Methodsput :: Putter (Var b a) #get :: Get (Var b a) # (NFData a, NFData b) => NFData (Var b a) Source # Instance detailsDefined in Bound.Var Methodsrnf :: Var b a -> () # (Eq b, Eq a) => Eq (Var b a) Source # Instance detailsDefined in Bound.Var Methods(==) :: Var b a -> Var b a -> Bool #(/=) :: Var b a -> Var b a -> Bool # (Ord b, Ord a) => Ord (Var b a) Source # Instance detailsDefined in Bound.Var Methodscompare :: Var b a -> Var b a -> Ordering #(<) :: Var b a -> Var b a -> Bool #(<=) :: Var b a -> Var b a -> Bool #(>) :: Var b a -> Var b a -> Bool #(>=) :: Var b a -> Var b a -> Bool #max :: Var b a -> Var b a -> Var b a #min :: Var b a -> Var b a -> Var b a # (Hashable b, Hashable a) => Hashable (Var b a) Source # Instance detailsDefined in Bound.Var MethodshashWithSalt :: Int -> Var b a -> Int #hash :: Var b a -> Int # type Rep1 (Var b :: Type -> Type) Source # Instance detailsDefined in Bound.Var type Rep1 (Var b :: Type -> Type) = D1 ('MetaData "Var" "Bound.Var" "bound-2.0.6-DS4BioScVXnFPwrI4Ruoth" 'False) (C1 ('MetaCons "B" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b)) :+: C1 ('MetaCons "F" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1)) type Rep (Var b a) Source # Instance detailsDefined in Bound.Var type Rep (Var b a) = D1 ('MetaData "Var" "Bound.Var" "bound-2.0.6-DS4BioScVXnFPwrI4Ruoth" 'False) (C1 ('MetaCons "B" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b)) :+: C1 ('MetaCons "F" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))) fromScope :: Monad f => Scope b f a -> f (Var b a) Source # fromScope quotients out the possible placements of F in Scope by distributing them all to the leaves. This yields a more traditional de Bruijn indexing scheme for bound variables. Since, fromScope . toScope ≡ id we know that fromScope . toScope . fromScope ≡ fromScope and therefore (toScope . fromScope) is idempotent. toScope :: Monad f => f (Var b a) -> Scope b f a Source # Convert from traditional de Bruijn to generalized de Bruijn indices. This requires a full tree traversal # Deriving instances Use to automatically derive Applicative and Monad instances for your datatype. Also works for components that are lists or instances of Functor, but still does not work for a great deal of other things. The deriving-compat package may be used to derive the Show1 and Read1 instances. Note that due to Template Haskell staging restrictions, we must define these instances within the same TH splice as the Show and Read instances. (This is needed for GHC 9.6 and later, where Show and Read are quantified superclasses of Show1 and Read1, respectively.) {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE TemplateHaskell #-} import Bound (Scope, makeBound) import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1) import Data.Deriving (deriveShow1, deriveRead1) data Exp a = V a | App (Exp a) (Exp a) | Lam (Scope () Exp a) | ND [Exp a] | I Int deriving (Functor) makeBound ''Exp concat$ sequence
[ deriveShow1 ''Exp
instance Show a => Show (Exp a) where showsPrec = showsPrec1
|]
]


and in GHCi

ghci> :set -XDeriveFunctor
ghci> import Bound                (Scope, makeBound)
ghci> :{
ghci| data Exp a = V a | App (Exp a) (Exp a) | Lam (Scope () Exp a) | ND [Exp a] | I Int deriving (Functor)
ghci| makeBound ''Exp
ghci| fmap concat $sequence [deriveShow1 ''Exp, deriveRead1 ''Exp, [d| instance Read a => Read (Exp a) where { readsPrec = readsPrec1 }; instance Show a => Show (Exp a) where { showsPrec = showsPrec1 } |]] ghci| :}  The Eq and Ord instances can be derived similarly: import Data.Functor.Classes (Eq1, Ord1, eq1, compare1) import Data.Deriving (deriveEq1, deriveOrd1) fmap concat$ sequence
[ deriveEq1 ''Exp
, deriveOrd1 ''Exp
, [d| instance Eq a => Eq (Exp a) where (==) = eq1
instance Ord a => Ord (Exp a) where compare = compare1
|]
]


or in GHCi:

ghci> import Data.Functor.Classes (Eq1, Ord1, eq1, compare1)
ghci> import Data.Deriving        (deriveEq1, deriveOrd1)
ghci> :{
ghci| fmap concat \$ sequence [deriveEq1 ''Exp, deriveOrd1 ''Exp, [d| instance Eq a => Eq (Exp a) where { (==) = eq1 }; instance Ord a => Ord (Exp a) where { compare = compare1 } |]]
ghci| :}


We cannot automatically derive Eq and Ord using the standard GHC mechanism, because instances require Exp to be a Monad:

instance (Monad f, Eq b, Eq1 f, Eq a)    => Eq (Scope b f a)
instance (Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a)