bound-simple-0.2.0.0: A lightweight implementation of 'bound'
Copyright (c) 2013 Edward Kmett 2021 Marco Zocca BSD github.com/ocramz experimental POSIX Safe-Inferred Haskell2010

Bound.Simple

Description

# Example

The whnf function in this example shows how to beta-reduce a term of the untyped lambda calculus.

Note : the Show instance of Exp depends on its Show1 instance (since Exp has one type parameter), which can be derived Generically. This works on most recent versions of GHC (>= 8.6.1).

Note 2 : the example below requires language extensions DeriveFunctor, DeriveFoldable, DeriveTraversable and DerivingVia.

import Bound.Simple (Scope, Bound(..), abstract1, instantiate1)
import Data.Functor.Classes (Show1)
import Data.Functor.Classes.Generic (Generically(..))

import GHC.Generics (Generic1)

infixl 9 :@
data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
deriving (Show, Functor, Foldable, Traversable, Generic1)
deriving (Show1) via Generically Exp

instance Applicative Exp where pure = V; k <*> m = ap k m

return = 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 (e1 :@ e2) = case whnf e1 of
Lam b -> whnf (instantiate1 e2 b)
f'    -> f' :@ e2
whnf e = e

main :: IO ()
main = do
let term = lam x (V x) :@ V y
print term         -- Lam (Scope (V (B ()))) :@ V y
print $whnf term -- V y  Synopsis # Documentation class Bound t where Source # Minimal complete definition Nothing Methods (>>>=) :: Monad f => t f a -> (a -> f c) -> t f c 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 (Scope b) Source # Instance detailsDefined in Bound.Simple Methods(>>>=) :: Monad f => Scope b f a -> (a -> f c) -> Scope b f c Source # data Scope b f a Source # Scope b f a is an f expression with bound variables in b, and free variables in a #### Instances Instances details  Bound (Scope b) Source # Instance detailsDefined in Bound.Simple Methods(>>>=) :: Monad f => Scope b f a -> (a -> f c) -> Scope b f c Source # Functor f => Generic1 (Scope b f :: Type -> Type) Source # Instance detailsDefined in Bound.Simple Associated Typestype Rep1 (Scope b f) :: k -> Type # Methodsfrom1 :: forall (a :: k). Scope b f a -> Rep1 (Scope b f) a #to1 :: forall (a :: k). Rep1 (Scope b f) a -> Scope b f a # Monad f => Monad (Scope b f) Source # The monad permits substitution on free variables, while preserving bound variables Instance detailsDefined in Bound.Simple Methods(>>=) :: Scope b f a -> (a -> Scope b f b0) -> Scope b f b0 #(>>) :: Scope b f a -> Scope b f b0 -> Scope b f b0 #return :: a -> Scope b f a # Functor f => Functor (Scope b f) Source # Instance detailsDefined in Bound.Simple Methodsfmap :: (a -> b0) -> Scope b f a -> Scope b f b0 #(<$) :: a -> Scope b f b0 -> Scope b f a # Monad f => Applicative (Scope b f) Source # Instance detailsDefined in Bound.Simple Methodspure :: a -> Scope b f a #(<*>) :: Scope b f (a -> b0) -> Scope b f a -> Scope b f b0 #liftA2 :: (a -> b0 -> c) -> Scope b f a -> Scope b f b0 -> Scope b f c #(*>) :: Scope b f a -> Scope b f b0 -> Scope b f b0 #(<*) :: Scope b f a -> Scope b f b0 -> Scope b f a # Foldable f => Foldable (Scope b f) Source # toList is provides a list (with duplicates) of the free variables Instance detailsDefined in Bound.Simple Methodsfold :: Monoid m => Scope b f m -> m #foldMap :: Monoid m => (a -> m) -> Scope b f a -> m #foldMap' :: Monoid m => (a -> m) -> Scope b f a -> m #foldr :: (a -> b0 -> b0) -> b0 -> Scope b f a -> b0 #foldr' :: (a -> b0 -> b0) -> b0 -> Scope b f a -> b0 #foldl :: (b0 -> a -> b0) -> b0 -> Scope b f a -> b0 #foldl' :: (b0 -> a -> b0) -> b0 -> Scope b f a -> b0 #foldr1 :: (a -> a -> a) -> Scope b f a -> a #foldl1 :: (a -> a -> a) -> Scope b f a -> a #toList :: Scope b f a -> [a] #null :: Scope b f a -> Bool #length :: Scope b f a -> Int #elem :: Eq a => a -> Scope b f a -> Bool #maximum :: Ord a => Scope b f a -> a #minimum :: Ord a => Scope b f a -> a #sum :: Num a => Scope b f a -> a #product :: Num a => Scope b f a -> a # Traversable f => Traversable (Scope b f) Source # Instance detailsDefined in Bound.Simple Methodstraverse :: Applicative f0 => (a -> f0 b0) -> Scope b f a -> f0 (Scope b f b0) #sequenceA :: Applicative f0 => Scope b f (f0 a) -> f0 (Scope b f a) #mapM :: Monad m => (a -> m b0) -> Scope b f a -> m (Scope b f b0) #sequence :: Monad m => Scope b f (m a) -> m (Scope b f a) # (Functor f, Eq1 f, Eq b) => Eq1 (Scope b f) Source # Instance detailsDefined in Bound.Simple MethodsliftEq :: (a -> b0 -> Bool) -> Scope b f a -> Scope b f b0 -> Bool # (Functor f, Show1 f, Show b) => Show1 (Scope b f) Source # Instance detailsDefined in Bound.Simple MethodsliftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Scope b f a -> ShowS #liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Scope b f a] -> ShowS # (Eq e, Functor m, Eq1 m, Eq a) => Eq (Scope e m a) Source # Instance detailsDefined in Bound.Simple Methods(==) :: Scope e m a -> Scope e m a -> Bool #(/=) :: Scope e m a -> Scope e m a -> Bool # (Show e, Functor m, Show1 m, Show a) => Show (Scope e m a) Source # Instance detailsDefined in Bound.Simple MethodsshowsPrec :: Int -> Scope e m a -> ShowS #show :: Scope e m a -> String #showList :: [Scope e m a] -> ShowS # type Rep1 (Scope b f :: Type -> Type) Source # Instance detailsDefined in Bound.Simple type Rep1 (Scope b f :: Type -> Type) = D1 ('MetaData "Scope" "Bound.Simple" "bound-simple-0.2.0.0-4iD2bfDGGww6cAmTRQGquA" 'True) (C1 ('MetaCons "Scope" 'PrefixI 'True) (S1 ('MetaSel ('Just "unscope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (f :.: Rec1 (Var b))))

toScope :: f (Var b a) -> Scope b f a Source #

toScope is just another name for Scope

fromScope :: Scope b f a -> f (Var b a) Source #

fromScope is just another name for unscope

data Var b a Source #

#### Instances

Instances details
 Source # Instance detailsDefined in Bound.Simple MethodsliftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> Var a c -> Var b d -> Bool # Source # Instance detailsDefined in Bound.Simple 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 # Functor (Var b) Source # Instance detailsDefined in Bound.Simple Methodsfmap :: (a -> b0) -> Var b a -> Var b b0 #(<$) :: a -> Var b b0 -> Var b a # Foldable (Var b) Source # Instance detailsDefined in Bound.Simple 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 # Source # Instance detailsDefined in Bound.Simple 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) # Eq b => Eq1 (Var b) Source # Instance detailsDefined in Bound.Simple MethodsliftEq :: (a -> b0 -> Bool) -> Var b a -> Var b b0 -> Bool # Show b => Show1 (Var b) Source # Instance detailsDefined in Bound.Simple MethodsliftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Var b a -> ShowS #liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Var b a] -> ShowS # (Eq b, Eq a) => Eq (Var b a) Source # Instance detailsDefined in Bound.Simple Methods(==) :: Var b a -> Var b a -> Bool #(/=) :: Var b a -> Var b a -> Bool # (Show b, Show a) => Show (Var b a) Source # Instance detailsDefined in Bound.Simple MethodsshowsPrec :: Int -> Var b a -> ShowS #show :: Var b a -> String #showList :: [Var b a] -> ShowS # # Abstraction abstract :: Functor 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 :: (Functor 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 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"


bindings :: Foldable f => Scope b f a -> [b] Source #

Return a list of occurences of the variables bound by this Scope.

hoistScope :: (f (Var b a) -> g (Var b a)) -> Scope b f a -> Scope b g a Source #

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]


substitute :: (Monad f, Eq a) => a -> f a -> f a -> f a Source #

substitute a p w replaces the free variable a with p in w.

>>> substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]
["goodnight","Gracie","!!!"]


substituteVar :: (Functor f, Eq a) => a -> a -> f a -> f a Source #

substituteVar a b w replaces a free variable a with another free variable b in w.

>>> substituteVar "Alice" "Bob" ["Alice","Bob","Charlie"]
["Bob","Bob","Charlie"]


## Predicates

isClosed :: Foldable f => f a -> Bool Source #

A closed term has no free variables.

>>> isClosed []
True

>>> isClosed [1,2,3]
False


# Utils

newtype Generically f a Source #

Used with the DerivingVia extension to provide fast derivations for Eq1, Show1, and Ord1.

Constructors

 Generically FieldsunGenerically :: f a

#### Instances

Instances details
 (Generic1 f, GEq1 (Rep1 f)) => Eq1 (Generically f) Source # Instance detailsDefined in Data.Functor.Classes.Generic MethodsliftEq :: (a -> b -> Bool) -> Generically f a -> Generically f b -> Bool # (Generic1 f, GEq1 (Rep1 f), GOrd1 (Rep1 f)) => Ord1 (Generically f) Source # Instance detailsDefined in Data.Functor.Classes.Generic MethodsliftCompare :: (a -> b -> Ordering) -> Generically f a -> Generically f b -> Ordering # (Generic1 f, GShow1 (Rep1 f)) => Show1 (Generically f) Source # Instance detailsDefined in Data.Functor.Classes.Generic MethodsliftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Generically f a -> ShowS #liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Generically f a] -> ShowS #