Language.Nominal.Unify

Unification by permutation

Documentation

>>> import Data.Set as S

newtype KRen s

An element of KRen is either

1. Just an injective finite map from KAtom to KAtom (for this file, call this a renaming), or
2. A "nomap" value (Nothing).

A KRen represents a solution to the problem

does there exist a permutation that makes x equal to y?

A type in the KUnifyPerm typeclass is structurally guaranteed to give at most one solution to such a unification problem, up to renaming irrelevant atoms. So in a nutshell: names, lists, and tuples are good here, and functions (not an equality type) and sets (may have multiple solutions) are not good.

A Just value represents a solution to this unification problem; a Nothing value represents that no such solution can be found. unifyPerm calculates these solutions.

Constructors

Ren

Fields

• unRen :: Maybe (Map (KAtom s) (KAtom s))

Instances

Typeable s => KRestrict s (KRen s)

There are two reasonable notions of restriction; filter, or default to Nothing. We choose the option that discards minimal information, i.e. the filter.

Defined in Language.Nominal.Unify

Methods

restrict :: [KAtom s] -> KRen s -> KRen s

Typeable s => KSupport s (KRen s)

Support of a renaming is the set of nontrivially mapped atoms

>>> (supp (idRen :: Ren)) == S.empty
True
>>> (supp (nothingRen :: Ren)) == S.empty
True

Defined in Language.Nominal.Unify

Methods

ksupp :: proxy s -> KRen s -> Set (KAtom s)

Eq (KRen s)

Elements of KRen are compared for equality on their nub renNub, meaning just that identity mappings are ignored.

>>> a = exit $ freshAtom
>>> idRen == renExtend a a idRen
True 

Defined in Language.Nominal.Unify

Methods

(==) :: KRen s -> KRen s -> Bool

(/=) :: KRen s -> KRen s -> Bool

Ord (KRen s)

Elements of KRen are compared on their nub renNub, meaning just that identity mappings are ignored.

Defined in Language.Nominal.Unify

Methods

compare :: KRen s -> KRen s -> Ordering

(<) :: KRen s -> KRen s -> Bool

(<=) :: KRen s -> KRen s -> Bool

(>) :: KRen s -> KRen s -> Bool

(>=) :: KRen s -> KRen s -> Bool

max :: KRen s -> KRen s -> KRen s

min :: KRen s -> KRen s -> KRen s

Show (KRen s)

Defined in Language.Nominal.Unify

Methods

showsPrec :: Int -> KRen s -> ShowS

show :: KRen s -> String

showList :: [KRen s] -> ShowS

Generic (KRen s)

Defined in Language.Nominal.Unify

Associated Types

type Rep (KRen s) :: Type -> Type

Methods

from :: KRen s -> Rep (KRen s) x

to :: Rep (KRen s) x -> KRen s

Semigroup (KRen s)

Defined in Language.Nominal.Unify

Methods

(<>) :: KRen s -> KRen s -> KRen s

sconcat :: NonEmpty (KRen s) -> KRen s

stimes :: Integral b => b -> KRen s -> KRen s

Monoid (KRen s)

Defined in Language.Nominal.Unify

Methods

mempty :: KRen s

mappend :: KRen s -> KRen s -> KRen s

mconcat :: [KRen s] -> KRen s

Typeable s => Swappable (KRen s)

Defined in Language.Nominal.Unify

Methods

kswp :: Typeable s0 => KAtom s0 -> KAtom s0 -> KRen s -> KRen s

type Rep (KRen s)

Defined in Language.Nominal.Unify

type Rep (KRen s) = D1 (MetaData "KRen" "Language.Nominal.Unify" "nom-0.1.0.2-Cei0dwnsIrWHLKrPA11A4S" True) (C1 (MetaCons "Ren" PrefixI True) (S1 (MetaSel (Just "unRen") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Map (KAtom s) (KAtom s))))))

type Ren = KRen Tom

Renaming on a Tom instance

idRen :: KRen s

The identity renaming.

nothingRen :: KRen s

The Nothing renaming. If we think of KRen s as type of solutions to permutation unification problems, then nothingRen indicates no solution could be found.

isJustRen :: KRen s -> Bool

Is it Just a renaming? (My unification problem can be solved, and here's the solution.)

isNothingRen :: KRen s -> Bool

Is it Nothing? (Nope; no solution exists.)

renNub :: KRen s -> KRen s

The parts of the map that are not identity

renExtend :: KAtom s -> KAtom s -> KRen s -> KRen s

Extend a renaming m with a new pair a -> b, maintaining the property of being a partial injection. If adding a->b would destroy partial injectivity, then return Nothing.

renToList :: KRen s -> Maybe [(KAtom s, KAtom s)]

Extract the graph of a KRen, Maybe.

renFromList :: [(KAtom s, KAtom s)] -> KRen s

Convert a graph to a KRen.

renRemoveBlock :: [KAtom s] -> KRen s -> KRen s

Given a block of atoms, remove them from the map provided that the atoms in that block only map to other atoms within it; if an atom gets mapped across the block boundary, return Nothing.

Needed for equality instance of Chunk.

Unification up to a KRen

class KSupport s a => KUnifyPerm s a where

Equal-up-to-permutation. The algorithm works very simply by traversing the element looking for atoms and when it finds them, trying to match them up. If it can do so injectively then it succeeds with Just a renaming; if it fails it returns Nothing.

Question: Granted that KUnifyPerm is a subset of KSupport, why are they not equal? Because for simplicity we only consider types for which at most one unifier can be found, by an efficient structural traversal. This avoids backtracking, and makes a kunifyPerm a function to KRen. So, a key difference is that KSupport can easily calculate the support of a set (unordered list without multiplicities) whereas KUnifyPerm does not even attempt to calculate unifiers of sets; not because this would be impossible, but because it would require a significant leap in complexity that we do not seem to need (so far).

Minimal complete definition

Nothing

Methods

kunifyPerm :: proxy s -> a -> a -> KRen s

This calculates a solution to a unification problem

kunifyPerm :: (Generic a, GUnifyPerm s (Rep a)) => proxy s -> a -> a -> KRen s

This calculates a solution to a unification problem

ren :: KRen s -> a -> a

This applies a solution to a unification problem (represented as a renaming) to an element.

Note: ren is not just swapping. It traverses the structure of its argument performing an atom-for-atom renaming. In the case that its argument solves a unification problem, its effect is the same as if a permuatation were applied.

This is checked in iprop_fresh_ren and prop_unify_ren.

ren :: (Generic a, GUnifyPerm s (Rep a)) => KRen s -> a -> a

This applies a solution to a unification problem (represented as a renaming) to an element.

Note: ren is not just swapping. It traverses the structure of its argument performing an atom-for-atom renaming. In the case that its argument solves a unification problem, its effect is the same as if a permuatation were applied.

This is checked in iprop_fresh_ren and prop_unify_ren.

Instances

Typeable s => KUnifyPerm s Integer

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> Integer -> Integer -> KRen s

ren :: KRen s -> Integer -> Integer

Typeable s => KUnifyPerm s Int

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> Int -> Int -> KRen s

ren :: KRen s -> Int -> Int

Typeable s => KUnifyPerm s Char

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> Char -> Char -> KRen s

ren :: KRen s -> Char -> Char

Typeable s => KUnifyPerm s Bool

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> Bool -> Bool -> KRen s

ren :: KRen s -> Bool -> Bool

Typeable s => KUnifyPerm s ()

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> () -> () -> KRen s

ren :: KRen s -> () -> ()

(Typeable s, Typeable t) => KUnifyPerm s (KAtom t)

Unify atoms

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> KAtom t -> KAtom t -> KRen s

ren :: KRen s -> KAtom t -> KAtom t

KUnifyPerm s a => KUnifyPerm s (Maybe a)

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> Maybe a -> Maybe a -> KRen s

ren :: KRen s -> Maybe a -> Maybe a

KUnifyPerm s a => KUnifyPerm s (NonEmpty a)

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> NonEmpty a -> NonEmpty a -> KRen s

ren :: KRen s -> NonEmpty a -> NonEmpty a

KUnifyPerm s a => KUnifyPerm s [a]

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> [a] -> [a] -> KRen s

ren :: KRen s -> [a] -> [a]

(Typeable s, Eq a) => KUnifyPerm s (Nameless a)

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> Nameless a -> Nameless a -> KRen s

ren :: KRen s -> Nameless a -> Nameless a

UnifyPerm r => KUnifyPerm Tom (Input r)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> Input r -> Input r -> KRen Tom

ren :: KRen Tom -> Input r -> Input r

(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

(Typeable s, KUnifyPerm s a) => KUnifyPerm s (KNom s a)

Unify KNom abstractions. Unpack, unify, clean out fresh names

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> KNom s a -> KNom s a -> KRen s

ren :: KRen s -> KNom s a -> KNom s a

(Typeable s, Typeable u, KUnifyPerm s t) => KUnifyPerm s (KName u t)

Unify names: they behave just an atom-label tuple

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> KName u t -> KName u t -> KRen s

ren :: KRen s -> KName u t -> KName u t

(KUnifyPerm s a, KUnifyPerm s b) => KUnifyPerm s (Either a b)

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> Either a b -> Either a b -> KRen s

ren :: KRen s -> Either a b -> Either a b

(KUnifyPerm s a, KUnifyPerm s b) => KUnifyPerm s (a, b)

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> (a, b) -> (a, b) -> KRen s

ren :: KRen s -> (a, b) -> (a, b)

(UnifyPerm r, UnifyPerm d) => KUnifyPerm Tom (ValFin r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> ValFin r d -> ValFin r d -> KRen Tom

ren :: KRen Tom -> ValFin r d -> ValFin r d

KUnifyPerm Tom (ValTriv r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> ValTriv r d -> ValTriv r d -> KRen Tom

ren :: KRen Tom -> ValTriv r d -> ValTriv r d

(UnifyPerm d, UnifyPerm v) => KUnifyPerm Tom (Output d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> Output d v -> Output d v -> KRen Tom

ren :: KRen Tom -> Output d v -> Output d v

(KUnifyPerm s a, KUnifyPerm s b, KUnifyPerm s c) => KUnifyPerm s (a, b, c)

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> (a, b, c) -> (a, b, c) -> KRen s

ren :: KRen s -> (a, b, c) -> (a, b, c)

(KUnifyPerm s a, KUnifyPerm s b, Eq b) => KUnifyPerm s (KEvFinMap s a b)

Defined in Language.Nominal.Equivar

Methods

kunifyPerm :: proxy s -> KEvFinMap s a b -> KEvFinMap s a b -> KRen s

ren :: KRen s -> KEvFinMap s a b -> KEvFinMap s a b

(UnifyPerm r, UnifyPerm d, UnifyPerm v) => KUnifyPerm Tom (Blockchain r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> Blockchain r d v -> Blockchain r d v -> KRen Tom

ren :: KRen Tom -> Blockchain r d v -> Blockchain r d v

(UnifyPerm r, UnifyPerm d, UnifyPerm v) => KUnifyPerm Tom (Chunk r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> Chunk r d v -> Chunk r d v -> KRen Tom

ren :: KRen Tom -> Chunk r d v -> Chunk r d v

(UnifyPerm d, UnifyPerm r, UnifyPerm v) => KUnifyPerm Tom (Context r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> Context r d v -> Context r d v -> KRen Tom

ren :: KRen Tom -> Context r d v -> Context r d v

(UnifyPerm d, UnifyPerm r, UnifyPerm v) => KUnifyPerm Tom (Transaction r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> Transaction r d v -> Transaction r d v -> KRen Tom

ren :: KRen Tom -> Transaction r d v -> Transaction r d v

(KUnifyPerm s a, KUnifyPerm s b, KUnifyPerm s c, KUnifyPerm s d) => KUnifyPerm s (a, b, c, d)

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> (a, b, c, d) -> (a, b, c, d) -> KRen s

ren :: KRen s -> (a, b, c, d) -> (a, b, c, d)

(KUnifyPerm s a, KUnifyPerm s b, KUnifyPerm s c, KUnifyPerm s d, KUnifyPerm s e) => KUnifyPerm s (a, b, c, d, e)

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> (a, b, c, d, e) -> (a, b, c, d, e) -> KRen s

ren :: KRen s -> (a, b, c, d, e) -> (a, b, c, d, e)

type UnifyPerm = KUnifyPerm Tom

Tom-instance of typeclass KUnifyPerm.

unifyPerm :: UnifyPerm a => a -> a -> Ren

Unify on KAtoms, thus Tom-instance of kunifyPerm.

kunifiablePerm :: KUnifyPerm s a => proxy s -> a -> a -> Bool

Does an s-unifier exist?

We write proxy instead of Proxy for the user's convenience, so the user can take advantage of any type that mentions s.

unifiablePerm :: UnifyPerm a => a -> a -> Bool

Does a Tom-unifier exist?

Special case: unifying prefixes of lists

kevPrefixRen :: KUnifyPerm s a => proxy s -> [a] -> [a] -> KRen s

Unify a list with a prefix of the other

evPrefixRen :: UnifyPerm a => [a] -> [a] -> Ren

Unify a list with a prefix of the other (at Tom version).

kevIsPrefix :: forall s proxy a. KUnifyPerm s a => proxy s -> [a] -> [a] -> Bool

One list unifies with a prefix of the other

evIsPrefix :: UnifyPerm a => [a] -> [a] -> Bool

One list unifies with a prefix of the other (at Tom version).

Tests

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