Language.Nominal.Abs

Name-abstraction, nominal style. This captures the "a." in "λa.ab".

Examples of practical usage are in Language.Nominal.Examples.SystemF, e.g. the type and term datatypes Typ and Trm.

Name-abstraction

data KAbs n a

A datatype for name-abstractions.

• KAbs n a is a type for abstractions of as by n-names, where we intend that n = KName s t for some s-atoms (atoms of type s) and t-labels (labels of type t).
• Abs t a is a type for abstractions of as by t-labelled Tom-atoms.

Under the hood an abstraction is just an element of (n, n -> a), but we do not expose this. What makes the type interesting is its constructor, abst :: KName s t -> a -> KAbs (KName s t) a, which is the only way to build an abstraction.

It's possible to implement KAbs using KNom — see absToNom and nomToAbs — but this requires a KSwappable typeclass constraint on a, which we prefer to avoid so that e.g. KAbs can be a Functor.

Instances

(KSupport s a, KSupport s t) => KSupport s (KAbs (KName s t) a)

Support of a :@> x is the support of x minus a

Defined in Language.Nominal.Abs

Methods

ksupp :: proxy s -> KAbs (KName s t) a -> Set (KAtom s)

(Typeable s, KUnifyPerm s t, KUnifyPerm s a) => KUnifyPerm s (KAbs (KName s t) a)

Unify Abs name-abstraction

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> KAbs (KName s t) a -> KAbs (KName s t) a -> KRen s

ren :: KRen s -> KAbs (KName s t) a -> KAbs (KName s t) a

Functor (KAbs n)

Defined in Language.Nominal.Abs

Methods

fmap :: (a -> b) -> KAbs n a -> KAbs n b

(<$) :: a -> KAbs n b -> KAbs n a

Default t => Applicative (KAbs (KName s t))

Defined in Language.Nominal.Abs

Methods

pure :: a -> KAbs (KName s t) a

(<*>) :: KAbs (KName s t) (a -> b) -> KAbs (KName s t) a -> KAbs (KName s t) b

liftA2 :: (a -> b -> c) -> KAbs (KName s t) a -> KAbs (KName s t) b -> KAbs (KName s t) c

(*>) :: KAbs (KName s t) a -> KAbs (KName s t) b -> KAbs (KName s t) b

(<*) :: KAbs (KName s t) a -> KAbs (KName s t) b -> KAbs (KName s t) a

(Typeable s, Swappable t, Eq t, Eq a) => Eq (KAbs (KName s t) a)

Abstractions are equal up to fusing their abstracted names.

Defined in Language.Nominal.Abs

Methods

(==) :: KAbs (KName s t) a -> KAbs (KName s t) a -> Bool

(/=) :: KAbs (KName s t) a -> KAbs (KName s t) a -> Bool

(Typeable s, Swappable t, Swappable a, Show t, Show a) => Show (KAbs (KName s t) a)

We show an abstraction by evaluating the function inside Abs on a fresh name (with the default Nothing label)

Defined in Language.Nominal.Abs

Methods

showsPrec :: Int -> KAbs (KName s t) a -> ShowS

show :: KAbs (KName s t) a -> String

showList :: [KAbs (KName s t) a] -> ShowS

Generic (KAbs n a)

Defined in Language.Nominal.Abs

Associated Types

type Rep (KAbs n a) :: Type -> Type

Methods

from :: KAbs n a -> Rep (KAbs n a) x

to :: Rep (KAbs n a) x -> KAbs n a

(Typeable s, Swappable t, Swappable a, Arbitrary (KName s t), Arbitrary a) => Arbitrary (KAbs (KName s t) a)

Defined in Language.Nominal.Properties.SpecUtilities

Methods

arbitrary :: Gen (KAbs (KName s t) a)

shrink :: KAbs (KName s t) a -> [KAbs (KName s t) a]

(Swappable n, Swappable a) => Swappable (KAbs n a)

Spelling out the generic swapping action for clarity, where we write KA for the (internal) constructor for KAbs: kswp n1 n2 (KA n f) = KA (kswp n1 n2 n) (kswp n1 n2 f)

Defined in Language.Nominal.Abs

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> KAbs n a -> KAbs n a

Binder (KAbs n a) n a s => BinderConc (KAbs n a) n a s n

Concretes an abstraction at a particular name. Unsafe if the name is not fresh.

(abst a x) `conc` a == x

abst a (x `conc` a) == x -- provided a is suitably fresh. 

new' $ \a -> abst a (x `conc` a) == x  

Defined in Language.Nominal.Abs

Methods

conc :: KAbs n a -> n -> a

cnoc :: n -> KAbs n a -> a

(Typeable s, Typeable u, KSub (KName s n) x t, KSub (KName s n) x y, Swappable t, Swappable y) => KSub (KName s n) x (KAbs (KName u t) y)

sub on a nominal abstraction substitutes in the label, and substitutes capture-avoidingly in the body

Defined in Language.Nominal.Sub

Methods

sub :: KName s n -> x -> KAbs (KName u t) y -> KAbs (KName u t) y

(Typeable s, Swappable t, Swappable a) => Binder (KAbs (KName s t) a) (KName s t) a s

Acts on an abstraction x' by unpacking x' as (n,x) for a fresh name n, and calculating f n x.

Defined in Language.Nominal.Abs

Methods

(@@) :: KAbs (KName s t) a -> (KName s t -> a -> b) -> KNom s b

(@>) :: KName s t -> a -> KAbs (KName s t) a

resMay :: KName s t -> a -> Maybe (KAbs (KName s t) a)

(Typeable s, Swappable n, Swappable x, Swappable y, KSub (KName s n) x y) => BinderConc (KAbs (KName s n) y) (KName s n) y s x

Nameless form of substitution, where the name for which we substitute is packaged in a KAbs abstraction.

Defined in Language.Nominal.Sub

Methods

conc :: KAbs (KName s n) y -> x -> y

cnoc :: x -> KAbs (KName s n) y -> y

type Rep (KAbs n a)

Defined in Language.Nominal.Abs

type Rep (KAbs n a) = D1 (MetaData "KAbs" "Language.Nominal.Abs" "nom-0.1.0.2-Cei0dwnsIrWHLKrPA11A4S" False) (C1 (MetaCons "AbsWrapper" PrefixI True) (S1 (MetaSel (Just "absName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 n) :*: S1 (MetaSel (Just "absApp") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (n -> a))))

type Abs t a = KAbs (KName Tom t) a

Abstraction by Tom-names.

Abstractions (basic functions)

abst :: (Typeable s, Swappable t, Swappable a) => KName s t -> a -> KAbs (KName s t) a

Create an abstraction by providing a name and a datum in which that name can be swapped (straight out of the paper; publisher and author's pdfs).

Instance of @>, for the case of a nominal abstraction.

abst' :: (Typeable s, Swappable t, Swappable a) => t -> KAtom s -> a -> KAbs (KName s t) a

A KName is just a pair of a label and an KAtom. This version of abst that takes a label and an atom, instead of a name.

pattern (:@>) :: (Typeable s, Swappable t, Swappable a) => KName s t -> a -> KAbs (KName s t) a infixr 0

The abstraction pattern '(:>)' is just an instance of '(:@!)' for KAbs. Thus,

n :@> x -> f n x

is synonymous with

x' -> x' @@! f 

Because '(:>)' is a concrete instance of '(:!)', we can declare it COMPLETE@.

fuse :: (KAbs (KName s t) a1, KAbs (KName s t) a2) -> KAbs (KName s t) (a1, a2)

Fuse abstractions, taking label of abstracted name from first argument. Should satisfy:

fuse (n @> x) (n @> y) = n @> (x, y)

unfuse :: KAbs (KName s t) (a, b) -> (KAbs (KName s t) a, KAbs (KName s t) b)

Split two abstractions. Should satisfy:

unfuse (n @> (x,y)) = (n @> x, n @> y)

absLabel :: KAbs (KName s t) a -> t

Return the label of an abstraction.

Note: For reasons having to do with the Haskell type system it's convenient to store this label in the underlying representation of the abstraction, using a "dummy name". However, we do not export access to this name, we only export access to its label, using absLabel.

conc :: BinderConc ctxbody ctx body s a => ctxbody -> a -> body

The bijection between Abs and KNom

absToNom :: (Typeable s, Swappable t, Swappable a) => KAbs (KName s t) a -> KNom s (KName s t, a)

Bijection between Nom and Abs. Just an instance of binderToNom.

nomToAbs :: (Typeable s, Swappable t, Swappable a) => KNom s (KName s t, a) -> KAbs (KName s t) a

Bijection between Nom and Abs. Just an instance of nomToBinder.

Unpacking name-contexts and abstractions

absFresh :: (Typeable s, Swappable t, Swappable a) => t -> (KName s t -> a) -> KAbs (KName s t) a

Apply f to a fresh element with label t

absFresh' :: (Typeable s, Swappable t, Swappable a, Default t) => (KName s t -> a) -> KAbs (KName s t) a

Apply f to a fresh element with default label

absFuncOut :: (Typeable s, Swappable t, Swappable a, Swappable b, Default t) => (KAbs (KName s t) a -> KAbs (KName s t) b) -> KAbs (KName s t) (a -> b)

Near inverse to applicative distribution. absFuncIn . absFuncOut = id but not necessarily other way around

Tests

Property-based tests are in Language.Nominal.Properties.AbsSpec.