Copyright	(C) 2013 Edward Kmett (C) 2021 Marco Zocca (ocramz)
License	BSD-style (see the file LICENSE)
Maintainer	ocramz
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Bound.Simple

Contents

Abstraction
Instantiation
- Predicates
Utils

Description

Scope is to be used inside of the definition of binders.

A lightweight implementation of bound. Provides much of the functionality of Bound.Scope.Simple, without the large dependency footprint.

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 thanks to DerivingVia. This works on most recent versions of GHC (>= 8.6.1).

{--}
{--}
{--}

import Bound.Simple (Scope, Bound(..), abstract1, instantiate1)
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

instance Monad Exp where
  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

class Bound t where
- (>>>=) :: Monad f => t f a -> (a -> f c) -> t f c
data Scope b f a
toScope :: f (Var b a) -> Scope b f a
fromScope :: Scope b f a -> f (Var b a)
data Var b a
abstract :: Functor f => (a -> Maybe b) -> f a -> Scope b f a
abstract1 :: (Functor 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
bindings :: Foldable f => Scope b f a -> [b]
hoistScope :: (f (Var b a) -> g (Var b a)) -> Scope b f a -> Scope b g a
closed :: Traversable f => f a -> Maybe (f b)
substitute :: (Monad f, Eq a) => a -> f a -> f a -> f a
substituteVar :: (Functor f, Eq a) => a -> a -> f a -> f a
isClosed :: Foldable f => f a -> Bool
newtype Generically f a = Generically {
- unGenerically :: f a
}

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 details Defined 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 details Defined 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 details Defined in Bound.Simple Associated Types type Rep1 (Scope b f) :: k -> Type # Methods from1 :: 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 details Defined 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 details Defined in Bound.Simple Methods fmap :: (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 details Defined in Bound.Simple Methods pure :: 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 details Defined in Bound.Simple Methods fold :: 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 details Defined in Bound.Simple Methods traverse :: 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 details Defined in Bound.Simple Methods liftEq :: (a -> b0 -> Bool) -> Scope b f a -> Scope b f b0 -> Bool #
(Functor f, Show1 f, Show b) => Show1 (Scope b f) Source #
Instance details Defined in Bound.Simple Methods liftShowsPrec :: (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 details Defined 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 details Defined in Bound.Simple Methods showsPrec :: 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 details Defined in Bound.Simple type Rep1 (Scope b f :: Type -> Type) = D1 ('MetaData "Scope" "Bound.Simple" "bound-simple-0.1.0.0-8WxpELcM4nh6dCmAaAmaLC" '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

Eq2 Var Source #
Instance details Defined in Bound.Simple Methods liftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> Var a c -> Var b d -> Bool #
Show2 Var Source #
Instance details Defined in Bound.Simple Methods liftShowsPrec2 :: (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 details Defined in Bound.Simple Methods fmap :: (a -> b0) -> Var b a -> Var b b0 # (<$) :: a -> Var b b0 -> Var b a #
Foldable (Var b) Source #
Instance details Defined in Bound.Simple Methods fold :: 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 #
Traversable (Var b) Source #
Instance details Defined in Bound.Simple Methods traverse :: 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 details Defined in Bound.Simple Methods liftEq :: (a -> b0 -> Bool) -> Var b a -> Var b b0 -> Bool #
Show b => Show1 (Var b) Source #
Instance details Defined in Bound.Simple Methods liftShowsPrec :: (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 details Defined 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 details Defined in Bound.Simple Methods showsPrec :: 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
Fields unGenerically :: f a

Instances

Instances details

(Generic1 f, GEq1 (Rep1 f)) => Eq1 (Generically f) Source #
Instance details Defined in Data.Functor.Classes.Generic Methods liftEq :: (a -> b -> Bool) -> Generically f a -> Generically f b -> Bool #
(Generic1 f, GEq1 (Rep1 f), GOrd1 (Rep1 f)) => Ord1 (Generically f) Source #
Instance details Defined in Data.Functor.Classes.Generic Methods liftCompare :: (a -> b -> Ordering) -> Generically f a -> Generically f b -> Ordering #
(Generic1 f, GShow1 (Rep1 f)) => Show1 (Generically f) Source #
Instance details Defined in Data.Functor.Classes.Generic Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Generically f a -> ShowS # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Generically f a] -> ShowS #