Copyright	(c) Murdoch J. Gabbay 2020
License	GPL-3
Maintainer	murdoch.gabbay@gmail.com
Stability	experimental
Portability	POSIX
Safe Haskell	None
Language	Haskell2010

Language.Nominal.Abs

Contents

Name-abstraction
Abstractions (basic functions)
The bijection between Abs and KNom
Unpacking name-contexts and abstractions
Tests

Description

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.

Synopsis

data KAbs n a
type Abs t a = KAbs (KName Tom t) a
abst :: (Typeable s, Swappable t, Swappable a) => KName s t -> a -> KAbs (KName s t) a
abst' :: (Typeable s, Swappable t, Swappable a) => t -> KAtom s -> a -> KAbs (KName s t) a
pattern (:@>) :: (Typeable s, Swappable t, Swappable a) => KName s t -> a -> KAbs (KName s t) a
fuse :: (KAbs (KName s t) a1, KAbs (KName s t) a2) -> KAbs (KName s t) (a1, a2)
unfuse :: KAbs (KName s t) (a, b) -> (KAbs (KName s t) a, KAbs (KName s t) b)
absLabel :: KAbs (KName s t) a -> t
conc :: BinderConc ctxbody ctx body s a => ctxbody -> a -> body
absToNom :: (Typeable s, Swappable t, Swappable a) => KAbs (KName s t) a -> KNom s (KName s t, a)
nomToAbs :: (Typeable s, Swappable t, Swappable a) => KNom s (KName s t, a) -> KAbs (KName s t) a
absFresh :: (Typeable s, Swappable t, Swappable a) => t -> (KName s t -> a) -> KAbs (KName s t) a
absFresh' :: (Typeable s, Swappable t, Swappable a, Default t) => (KName s t -> a) -> KAbs (KName s t) a
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)

Name-abstraction

data KAbs n a Source #

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) Source #	Support of a :@> x is the support of x minus a
Instance details Defined in Language.Nominal.Abs Methods ksupp :: proxy s -> KAbs (KName s t) a -> Set (KAtom s) Source #
(Typeable s, KUnifyPerm s t, KUnifyPerm s a) => KUnifyPerm s (KAbs (KName s t) a) Source #	Unify `Abs` name-abstraction
Instance details Defined in Language.Nominal.Unify Methods kunifyPerm :: proxy s -> KAbs (KName s t) a -> KAbs (KName s t) a -> KRen s Source # ren :: KRen s -> KAbs (KName s t) a -> KAbs (KName s t) a Source #
Functor (KAbs n) Source #
Instance details 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)) Source #
Instance details 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) Source #	Abstractions are equal up to fusing their abstracted names.
Instance details 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) Source #	We show an abstraction by evaluating the function inside `Abs` on a fresh name (with the default `Nothing` label)
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #	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)`
Instance details Defined in Language.Nominal.Abs Methods kswp :: Typeable s => KAtom s -> KAtom s -> KAbs n a -> KAbs n a Source #
Binder (KAbs n a) n a s => BinderConc (KAbs n a) n a s n Source #	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
Instance details Defined in Language.Nominal.Abs Methods conc :: KAbs n a -> n -> a Source # cnoc :: n -> KAbs n a -> a Source #
(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) Source #	sub on a nominal abstraction substitutes in the label, and substitutes capture-avoidingly in the body
Instance details Defined in Language.Nominal.Sub Methods sub :: KName s n -> x -> KAbs (KName u t) y -> KAbs (KName u t) y Source #
(Typeable s, Swappable t, Swappable a) => Binder (KAbs (KName s t) a) (KName s t) a s Source #	Acts on an abstraction `x'` by unpacking `x'` as `(n,x)` for a fresh name `n`, and calculating `f n x`.
Instance details Defined in Language.Nominal.Abs Methods (@@) :: KAbs (KName s t) a -> (KName s t -> a -> b) -> KNom s b Source # (@>) :: KName s t -> a -> KAbs (KName s t) a Source # resMay :: KName s t -> a -> Maybe (KAbs (KName s t) a) Source #
(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 Source #	Nameless form of substitution, where the name for which we substitute is packaged in a `KAbs` abstraction.
Instance details Defined in Language.Nominal.Sub Methods conc :: KAbs (KName s n) y -> x -> y Source # cnoc :: x -> KAbs (KName s n) y -> y Source #
type Rep (KAbs n a) Source #
Instance details Defined in Language.Nominal.Abs type Rep (KAbs n a) = D1 (MetaData "KAbs" "Language.Nominal.Abs" "nom-0.1.0.1-3UtpNOnqRlSC6EhVIia7SR" 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 Source #

Abstraction by Tom-names.

Abstractions (basic functions)

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

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

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

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

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

Split two abstractions. Should satisfy:

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

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

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

The bijection between `Abs` and `KNom`

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

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

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

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

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

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

Tests

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

Name-abstraction

Abstractions (basic functions)

The bijection between Abs and KNom

Unpacking name-contexts and abstractions

Tests

The bijection between `Abs` and `KNom`