KEvFun s a b is just a -> b in a wrapper. But, we give this wrapped function trivial swapping and support. (For a usage example see the source code for Val.)

Functions need not be finite and are not equality types in general, so we cannot computably test that the actual function wrapped by the programmer actually does have a trivial swapping action (i.e. really is equivariant).

It's the programmer's job to only insert truly equivariant functions here. Non-equivariant elements may lead to incorrect runtime behaviour.

On an equivariant orbit-finite type, the compiler can step in with more stringent guarantees. See e.g. KEvFinMap.

Tom-equivariant function-space

Filter a list down to one representative from each atoms-orbit (choosing first representative of each orbit).

Instance for Tom atom type.

Restrict a Map to its equivariant nub, discarding all but one of each key-orbit

Instance for unit atom type.

Equivariantly apply a map m to an element a.

• If a == ren r a' for some r :: Ren and m a' == b',
• then kevLookup m a == ren r b'.

For this to work, we require types a and b to support a ren action, meaning they should support notions of unification up to permutation.

kevLookup instantiated to a Tom.

Equivariantly apply a list of pairs, which we assume represents a map, to an element. Also returns the source element.

Equivariantly apply a list of pairs (which we assume represents a map), to an element

Equivariantly apply a list of pairs (which we assume represents a map), to an element. Tom version.

A type for orbit-finite equivariant maps.

KEvFinMap at a Tom. Thus, a type for orbit-finite Tom-equivariant maps.

Equivariant application of an orbit-finite map. Given a map (expressed as finitely many representative pairs) and an argument ...

• it tries to rename atoms to match the argument to the first element of one of its pairs and
• if it finds a match, it maps to the second element of that pair, suitably renamed.

A constant equivariant map. We assume the codomain is Nameless.

>>> (constEvFinMap 42 :: EvFinMap Char Int) $$ 'x'
42

>>> (constEvFinMap 0 :: EvFinMap Atom Int) $$ a
0 

Extends a map with a new orbit, by specifying a representative a maps to b. We assume codomain b is Nameless, as discussed above.

>>> (extEvFinMap 'x' 7 $ (constEvFinMap 42 :: EvFinMap Char Int)) $$ 'x'
7

>>> (extEvFinMap 'x' 7 $ (constEvFinMap 42 :: EvFinMap Char Int)) $$ 'y'
42

>>> let [m, n, o] = exit $ freshNames [(), (), ()]
>>> m == n
False
>>> unifiablePerm m n
True
>>> (extEvFinMap m 7 $ (constEvFinMap 42 :: EvFinMap (Name ()) Int)) $$ n
7
>>> (extEvFinMap o 8 (extEvFinMap m 7 $ (constEvFinMap 42 :: EvFinMap (Name ()) Int))) $$ n
8

Constructs an orbit-finite equivariant map by prescribing a default value, and finitely many argument-value pairs. We assume the codomain is Nameless, as discussed above.

>>> let f = evFinMap 42 [('x', 7), ('y', 5), ('x', 13)] :: EvFinMap Char Int
>>> map (f $$) ['x', 'y', 'z']
[13,5,42]

>>> let atmEq = evFinMap False [((a,a), True)] :: EvFinMap (Atom, Atom) Bool
>>> map (atmEq $$) [(b,b), (c,c), (a,c), (b,c)]
[True,True,False,False]

>>> let g = evFinMap 2 [((a,a), 0), ((b,c), 1)] :: EvFinMap (Atom, Atom) Int
>>> map (g $$) [(b,b), (c,c), (a,c), (b,c)]
[0,0,1,1]

Extracts default value und list of exceptional argument-value pairs from an EvFinMap.

>>> fromEvFinMap $ (evFinMap 42 [('x', 7), ('y', 5), ('x', 13)] :: EvFinMap Char Int)
(42,[('y',5),('x',13)])