2      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                  ! " # $ % & ' ( ) * + , - . / 0 1 SafeH RA name generator consists of a (possibly finite) list of name suggestions and an expander1, which is a function for generating more names.%A name suggestion is a list of possible names. When an atom must be renamed, the first useable name from the list is chosen. If the list is finite and contains no useable names, then additional names will be generated by appending numerical subscripts. To override this behavior, redefine   for the given AtomKind0 instance, or specify an infinite list of names./The names to use if nothing else was specified.Convert a digit to a subscript./Check if a character is a letter or underscore.ZGenerate an infinite list of possible names from a (possibly finite) list of suggestions.The default name generator. dCompute a string that is not in the given set, and whose name is based on the supplied suggestions. vMerge two name suggestions. Essentially this appends them, but we try to avoid duplication. We use the left expander.   SafeNone1x HA global variable holding a set of strings already used for free names. The use of 2p in this function is safe, because it is only called once and serves to create a unique global reference cell. Create a globally new concrete name based on the given name suggestion. This ensures that fresh names have distinct names when they are not bound. HCreate a globally new concrete name based on the given name suggestion. The use of 2u in this function is safe, provided that the user only uses API functions and respects Pitts's freshness condition.YPerform a subcomputation in the presence of a globally unique value. This is similar to 30, but uses a continuation monad instead of the 4` monad. To ensure referential transparency, the unique value must not escape the function body. The use of 2u in this function is safe, provided that the user only uses API functions and respects Pitts's freshness condition.Unsafely embed the 4 monad in a continuation monad. The use of 2u in this function is safe, provided that the user only uses API functions and respects Pitts's freshness condition.  NoneA +An atom is a globally unique, opaque value.^An atom consists of a unique identifier, a concrete name, and some optional name suggestions.Return the name of an atom.&Return the suggested names of an atom.GGlobally create a fresh atom with the given name and name suggestions.=Globally create a fresh atom with the given name suggestions.=Create a fresh atom with the given name and name suggestions.LThe correct use of this function is subject to Pitts's freshness condition.3Create a fresh atom with the given name suggestion.Here, the call to  & is performed lazily (outside of the 4E monad), so an actual concrete name will only be computed on demand.LThe correct use of this function is subject to Pitts's freshness condition.User code should not explicitly compare atoms for relative ordering, because this is not referentially transparent (can be unsound). However, we define an 5L instance for atoms anyway, because it permits atoms to be used as keys in Sets and Maps. NoneVA type synonym.lThe group of finitely supported permutations on atoms. This is an abstract type with no exposed structure. Implementation note: If we used  directly, inverting a permutation would be O(n). We make inverting O(1) by storing a permutation together with its inverse. Because of laziness, the inverse will not be computed unless it is used.7The monoid of finitely supported permutations on atoms. The identity permutation. O(1).!Compose two permutations. O(m) where m' is the size of the right permutation."Compose two permutations. O(n) where nm is the size of the left permutation. This also requires the inverse of the right permutation as an input.#%Apply a permutation to an atom. O(1).$Swap a and b. O(1).%)Return the domain of a permutation. O(n).&The identity permutation. O(1).'Compose two permutations. O(m) where m' is the size of the right permutation.(Compose two permutations. O(n) where n& is the size of the left permutation.)Invert a permutation. O(1).*%Apply a permutation to an atom. O(1).+Swap a and b. O(1).,Swap the given pairs of atoms.-The domain of a permutation. O(n)..OMake a permutation from a list of swaps. This is mostly useful for testing. O(n)./OTurn a permutation into a list of swaps. This is mostly useful for testing. O(n). !"#$%&'()*+,-./ !"#$%&'()*+,-./None7<ST 3A version of the ;( class suitable for generic programming.5A basic or  non-nominalc type is a type whose elements cannot contain any atoms. Typical examples are base types, such as 6 or 7>, and other types constructed exclusively from them, such as [6] or 7 -> 7:. On such types, the nominal structure is trivial, i.e.,  "x=x for all x.For convenience, we define 5^ as a wrapper around such types, which will automatically generate appropriate instances of ;, NominalSupport,  NominalShow, and Bindable*. You can use it, for example, like this: 8type Term = Var Atom | Const (Basic Int) | App Term Term"Some common base types, including 7, 8, 9, 6, :, ;, and <W are already instances of the relevant type classes, and do not need to be wrapped in 5. The use of 5; can sometimes have a performance advantage. For example, 5 = is a more efficient ; instance than =9. Although they are semantically equivalent, the use of 5f prevents having to traverse the string to check each character for atoms that are clearly not there.77 t is the type of atom abstractions, denoted [a]t in the nominal logic literature. Its elements are of the form (a.v) modulo alpha-equivalence. For full technical details on what this means, see Definition 4 of [Pitts 2002].Implementation note: we currently use an HOAS encoding, as this turns out to be far more efficient (both in time and memory usage) than the alternatives. An important invariant of the HOAS encoding is that the underlying function must only be applied to fresh atoms.99 t is the type t, but equipped with an explicit substitution. This is used to cache substitutions so that they can be optimized and applied all at once.;WA type is nominal if the group of finitely supported permutations of atoms acts on it.In most cases, instances of ;$ can be automatically derived. See  #DERIVING"Deriving generic instances"( for information on how to do so, and  #CUSTOM"Defining custom instances"$ for how to write custom instances.<'Apply a permutation of atoms to a term.=Apply a deferred permutation.>Atom abstraction: > a t- represents the equivalence class of pairs (a,t6) modulo alpha-equivalence. We first define this for  and later generalize to other Atomic types.?%Destructor for atom abstractions. If m=y.s , the term open m (\x t -> body)binds x to a fresh name and t to a term such that x.t=y.s.LThe correct use of this function is subject to Pitts's freshness condition.@0Merge two abstractions. The defining property is merge (x.t) (x.s) = (x.(t,s))AA helper function for defining ;" instances for non-nominal types.3456789:;<=>?@A/;<<9:=`78>?_^@56A]\[ZYXWVUTSRQPONMLKJIH34FEDCBG3456789:;<<None7<STdA version of the f( class suitable for generic programming.ff is a subclass of ;y consisting of those types for which the support can be calculated. With the notable exception of function types, most ; types are also instances of f.In most cases, instances of f$ can be automatically derived. See  #DERIVING"Deriving generic instances"( for information on how to do so, and  #CUSTOM"Defining custom instances"$ for how to write custom instances.g\Compute a set of atoms and strings that should not be used as the names of bound variables.hThis type provides an internal representation for the support of a nominal term, i.e., the set of atoms (and constants) occurring in it. This is an abstract type with no exposed structure. The only way to construct a value of type h is to use the function g.j3Something to be avoided can be an atom or a string.mA wrapper around strings. This is used to denote any literal strings whose values should not clash with the names of bound variables. For example, if a term contains a constant symbol c , the name cl should not also be used as the name of a bound variable. This can be achieved by marking the string with m , like this 3data Term = Var Atom | Const (Literal String) | ...Another way to use m! is in the definition of custom f instances. See  #CUSTOM"Defining custom instances" for an example.oThe empty support.p The union of a list of supports.qThe union of two supports.rAdd an atom to the support.sA singleton support.t Delete an atom from the support.u(Delete a list of atoms from the support.v$Add a literal string to the support.w)Convert the support to a list of strings.x A variant of open which moreover chooses a name for the bound atom that does not clash with any free name in its scope. This function is mostly useful for building custom pretty-printers for nominal terms. Except in pretty-printers, it is equivalent to open.Usage: +open_for_printing sup t (\x s sup' -> body)Here, sup=gt+. For printing to be efficient (roughly O(n)), the support must be pre-computed in a bottom-up fashion, and then passed into each subterm in a top-down fashion (rather than re-computing it at each level, which would be O(n)). For this reason, open_for_printing takes the support of t* as an additional argument, and provides sup', the support of s*, as an additional parameter to the body.0The correct use of this function is subject to  #CONDITIONPitts's freshness condition.yA helper function for defining f" instances for non-nominal types.defghijklmnopqrstuvwxy6mnzjklhiopqrstuvwfggxyde~}|{defgghijklmnNone %/678<STdA version of the ( class suitable for generic programming.The type constructor  permits data of arbitrary types (including nominal types) to be embedded in binders without becoming bound. For example, in the term m = (a, NoBind b).(a,b), the atom a is bound, but the atom b remains free. Thus, m is alpha-equivalent to (x, NoBind b).(x,b), but not to (x,NoBindc).(x,c).3A typical use case is using contexts as binders. A context3 is a map from atoms to some data (for example, a typing context' is a map from atoms to types, and an evaluation contextB is a map from atoms to values). If we define contexts like this: #type Context t = [(Atom, NoBind t)]<then we can use contexts as binders. Specifically, if ={x !A , &,x !A } is a context, then (.t) binds the context to a term t. This means, x , &,x are bound in t", but not any atoms that occur in A , &,A . Without the use of , any atoms occurring on A , &,A! would have been bound as well.Even though atoms under  are not binding, they can still be bound) by other binders. For example, the term x.(x,  x) is alpha-equivalent to y.(y,y)". Another way to say this is that D has a special behavior on the left, but not on the right of a dot. A type is C if its elements can be abstracted. Such elements are also called binders, or sometimes patterns?. Examples include atoms, tuples of atoms, list of atoms, etc.In most cases, instances of ;$ can be automatically derived. See  #DERIVING"Deriving generic instances"( for information on how to do so, and  #CUSTOM"Defining custom instances"$ for how to write custom instances.SA function that maps a term to a binder. New binders can be constructed using the > structure of . See  #CUSTOM"Defining custom instances" for examples. a t is the type of  abstractions , denoted [A]T; in the nominal logic literature. Its elements are pairs (a,t+) modulo alpha-equivalence. We also write ato for such an equivalence class of pairs. For full technical details on what this means, see Definition 4 of  #PITTS2003 [Pitts2003].$A representation of binders of type ab. This is an abstract type with no exposed structure. The only way to construct a value of type  a is through the >' interface and by using the functions  and .BThe type of abstractions of a list of atoms. It is equivalent to []t*, but has a more low-level implementation.9A pattern matching syntax for abstractions. The pattern (x:.t) is called an abstraction pattern. It matches any term of type ( a b)&. The result of matching the pattern (x:.t) against a value ys is to bind x to a fresh name and t to a value such that xt=ys. Note that a different fresh xO is chosen each time an abstraction patterns is used. Here are some examples: tfoo (x :. t) = body let (x :. t) = s in body case t of Var v -> body1 App m n -> body2 Abs (x :. t) -> body3CLike all patterns, abstraction patterns can be nested. For example: zfoo1 (a :. b :. t) = ... foo2 (x :. (s,t)) = (x.s, x.t) foo3 (Abs (x :. Var y)) | x == y = ... | otherwise = ... 7The correct use of abstraction patterns is subject to  #CONDITIONPitts's freshness condition1. Thus, for example, the following are permitted <let (x :. t) = s in x.t, let (x :. t) = s in f x t == g x t,'whereas the following is not permitted: let (x :. t) = s in (x,t).See  #CONDITION"Pitts's freshness condition" for more details.#Abstract a list of atoms in a term.Open a list abstraction.LThe correct use of this function is subject to Pitts's freshness condition.%Open a list abstraction for printing.LThe correct use of this function is subject to Pitts's freshness condition.RMerge a pair of list abstractions. If the lists are of different lengths, return ?.dConstructor for non-binding binders. This can be used to mark non-binding subterms when defining a  instance. See  #CUSTOM"Defining custom instances" for examples./Constructor for a binder binding a single atom.Map a function over a .Combinator giving H an applicative structure. This is used for constructing tuple binders.'Constructor for abstractions. The term at- represents the equivalence class of pairs (a,t) modulo alpha-equivalence.We use the infix operator (), which is normally bound to function composition in the standard Haskell library. Thus, nominal programs should import the standard library like this: import Prelude hiding ((.)) Note that ()# is a abstraction operator of the objectlanguage9 (i.e., whatever datatype you are defining), not of the  metalanguage! (i.e., Haskell). A term such as at# only makes sense if the variable a is already defined to be a particular atom. Thus, abstractions are often used in the context of a scoped operation such as  [ or on the right-hand side of an abstraction pattern match, as in the following examples: Hwith_fresh (\a -> a.a) subst m z (Abs (x :. t)) = Abs (x . subst m z t)ZFor building an abstraction by using a binder of the metalanguage, see also the function  .&An alternative non-infix notation for ()C. This can be useful when using qualified module names, because " Nominal.." is not valid syntax.1An alternative notation for abstraction patterns. f t = open t (\x s -> body)is precisely equivalent to f (x :. s) = body.0The correct use of this function is subject to  #CONDITIONPitts's freshness condition. A variant of  which moreover chooses a name for the bound atom that does not clash with any free name in its scope. This function is mostly useful for building custom pretty-printers for nominal terms. Except in pretty-printers, it is equivalent to .Usage: +open_for_printing sup t (\x s sup' -> body)Here, sup=gt (this requires a f5 instance). For printing to be efficient (roughly O(n)), the support must be pre-computed in a bottom-up fashion, and then passed into each subterm in a top-down fashion (rather than re-computing it at each level, which would be O(n)). For this reason,  takes the support of t* as an additional argument, and provides sup', the support of s*, as an additional parameter to the body.0The correct use of this function is subject to  #CONDITIONPitts's freshness condition.A helper function for defining " instances for non-nominal types. A specialized combinator. Although this functionality is expressible in terms of the applicative structure, we give a custom CPS-based implementation for performance reasons. It improves the overall performance by 14% (time) and 16% (space) in a typical benchmark.Function composition.RSince we hide (.) from the standard library, and the fully qualified name of the Prelude's dot operator, " Prelude..R", is not legal syntax, we provide '"' as an alternate notation for composition.>55 None68FTk/The type of atoms of a given kind. For example: Btype Variable = AtomOfKind VarName type Type = AtomOfKind TypeName\An atom kind is a type-level constant (typically an empty type) that is an instance of the q class. An atom kind is optionally equipped with a list of suggested names for this kind of atom. For example: Rdata VarName instance AtomKind VarName where suggested_names _ = ["x", "y", "z"] Tdata TypeName instance AtomKind TypeName where suggested_names _ = ["a", "b", "c"]?It is possible to have infinitely many atom kinds, for example: Gdata Zero data Succ a instance AtomKind Zero instance AtomKind (Succ a)EThen Zero, Succ Zero, Succ (Succ Zero), etc., will all be atom kinds.8An optional list of default names for this kind of atom.An optional function for generating infinitely many distinct names from a finite list of suggestions. The default behavior is to append numerical subscripts. For example, the names  [x,y,z] are by default expanded to ![x,y,z, x , y , z , x ,y , &]W, using Unicode for the subscripts. To use a a different naming convention, redefine .It is not strictly necessary for all of the returned names to be distinct; it is sufficient that there are infinitely many distinct ones._Example: the following generates new variable names by appending primes instead of subscripts: 9expand_names _ xs = ys where ys = xs ++ map (++ "'") ysA type class for atom types.KThe suggested way to define a type of atoms is to define a new empty type t that is an instance of . Optionally, a list of suggested names for the new atoms can be provided. (These will be used as the names of bound variables unless otherwise specified). Then  t is a new type of atoms. vdata VarName instance AtomKind VarName where suggested_names = ["x", "y", "z"] newtype Variable = AtomOfKind VarName-The default variable names for the atom type.Return the name of an atom.6Perform a computation in the presence of a fresh atom.0The correct use of this function is subject to  #CONDITIONPitts's freshness condition7. Thus, for example, the following uses are permitted: <with_fresh (\a -> f a == g a) with_fresh (\a -> a . f a b c)Here is an example of what is not permitted: with_fresh (\a -> a)See  #CONDITION"Pitts's freshness condition" for more details. A version of  that permits a suggested name to be given to the atom. The name is only a suggestion, and will be changed, if necessary, to avoid clashes.0The correct use of this function is subject to  #CONDITIONPitts's freshness condition. A version of x that permits a list of suggested names to be specified. The first suitable name in the list will be used if possible.0The correct use of this function is subject to  #CONDITIONPitts's freshness condition.8Generate a globally fresh atom of the given atomic type. A version of  that that permits a suggested name to be given to the atom. The name is only a suggestion, and will be changed, if necessary, when the atom is bound. A version of x that permits a list of suggested names to be specified. The first suitable name in the list will be used if possible.=A convenience function for constructing binders. We can write bind (\x -> t)'to denote the abstraction (x.t), where x is a fresh atom. A version of 5 that also takes a suggested name for the bound atom. A version of > that also take a list of suggested names for the bound atom.-Convert an atomic binding to an atom binding.-Convert an atom binding to an atomic binding.@Sometimes, it is necessary to open two abstractions, using the sameu fresh name for both of them. An example of this is the typing rule for lambda abstraction in dependent type theory: q Gamma, x:t |- e : s ------------------------------------ Gamma |- Lam (x.e) : Pi t (x.s)>In the bottom-up reading of this rule, we are given the terms Lam body and Pi t body', and we require a fresh name x and terms e, s such that body=(x.e) and body'=(x.s). Crucially, the same atom x should be used in both e and s-, because we subsequently need to check that e has type s! in some scope that is common to e and s.The N primitive permits us to deal with such situations. Its defining property is merge (x.e) (x.s) = (x.(e,s)).)We can therefore solve the above problem: +let (x :. (e,s)) = merge body body' in ....Moreover, the o primitive can be used to define other merge-like functionality. For example, it is easy to define a function ?merge_list :: (Atomic a, Nominal t) => [Bind a t] -> Bind a [t]in terms of it.Semantically, the 8 operation implements the isomorphism of nominal sets [A]T[A]S=[A](TS).If x and y1 are atoms with user-suggested concrete names and  (z.(t',s')) = merge (x.t) (y.s),then z/ will be preferably given the concrete name of x, but the concrete name of y will be used if the name of x would cause a clash.5Return the list of default names associated with the kind9 of the given atom (not the name(s) of the atom itself). None7;<=STA version of the  N class suitable for generic programming. The implementation uses ideas from Generics.Deriving.Show.CThis type keeps track of which separator to use for the next tuple.   is similar to @a, but with support for renaming of bound variables. With the exception of function types, most ; types are also instances of  .In most cases, instances of  $ can be automatically derived. See  #DERIVING"Deriving generic instances"( for information on how to do so, and  #CUSTOM"Defining custom instances"$ for how to write custom instances. A nominal version of A<. This function takes as its first argument the support of t<. This is then passed into the subterms, making printing O(n) instead of O(n).It is recommended to define a   instance, rather than a @L instance, for each nominal type, and then either automatically derive the @ instance, or define it using . For example: :instance Show MyType where showsPrec = nominal_showsPrecPlease note: in defining   , neither B nor  \ should be used for the recursive cases, or else the benefit of fast printing will be lost.  The method  j is provided to allow the programmer to give a specialized way of showing lists of values, similarly to C'. The principal use of this is in the   instance of the 8S type, so that strings are shown in double quotes, rather than as character lists. Like B5, but for nominal types. Normally all instances of   are also instances of @, so B! can usually be used instead of  ./This function can be used in the definition of @) instances for nominal types, like this: :instance Show MyType where showsPrec = nominal_showsPrecA helper function for defining  = instances for non-nominal types. This requires an existing @ instance.     1     10/.-,+*)('&%$#"!       NonedG256;<Afghmny    5;<<56fgghmn     AyD  !"#$%&'()*+*,,-./0123456789:;<=>?@ABBCCDD EFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqqrstuuvwxyz{|}~                                       ! " # $ % & ' ( ) * + , - . / 0 1234567869:;<=67>67?67@67A67B67CDEDFDGHIHJHKHLM&nominal-0.2.0.0-GZ6w56NCfcED1WEKXzjIsVNominal.GenericNominal.ConcreteNamesNominal.Unsafe Nominal.AtomNominal.PermutationNominal.NominalNominal.NominalSupportNominal.BindableNominal.AtomicNominal.NominalShowNominal expand_names with_freshbindbase GHC.GenericsGenericNameGenNameSuggestion default_names to_subscript isAlphaOrWildexpand_defaultdefault_namegen rename_fresh combine_names global_used global_new_io global_new with_unique unsafe_withAtom atom_show atom_namesfresh_atom_named fresh_atomwith_fresh_atom_namedwith_fresh_atom $fShowAtom $fOrdAtom$fEqAtom PermutationNominalPermutationPerm p_identity p_composeR p_composeL p_apply_atomp_swapp_domain perm_identity perm_composeR perm_composeL perm_invertperm_apply_atom perm_swap perm_swaps perm_domain perm_of_swaps swaps_of_perm$fEqPerm $fShowPerm$fEqNominalPermutationGNominalgbulletBasicBindAtomDefer•force atom_abst atom_open atom_merge basic_action $fGNominalM1 $fGNominal:+: $fGNominal:*: $fGNominalU1 $fGNominalV1 $fGNominalK1 $fNominalSet $fNominalMap $fNominal(->)$fNominalEither$fNominalMaybe$fNominal(,,,,,,)$fNominal(,,,,,)$fNominal(,,,,)$fNominal(,,,) $fNominal(,,) $fNominal(,) $fNominal() $fNominal[]$fNominalBasic$fNominalOrdering$fNominalFloat$fNominalDouble $fNominalChar $fNominalInt$fNominalInteger $fNominalBool $fNominalAtom$fNominalBindAtom $fEqBindAtom$fNominalDefer $fShowBasic $fEqBasic $fOrdBasicGNominalSupportgsupportNominalSupportsupportSupportAvoideeASLiteral support_emptysupport_unions support_unionsupport_insert support_atomsupport_deletesupport_deletessupport_stringstrings_of_supportatom_open_for_printing basic_support$fNominalLiteral$fGNominalSupportM1$fGNominalSupport:+:$fGNominalSupport:*:$fGNominalSupportU1$fGNominalSupportV1$fGNominalSupportK1$fNominalSupportSet$fNominalSupportMap$fNominalSupportDefer$fNominalSupportBindAtom$fNominalSupportEither$fNominalSupportMaybe$fNominalSupport(,,,,,,)$fNominalSupport(,,,,,)$fNominalSupport(,,,,)$fNominalSupport(,,,)$fNominalSupport(,,)$fNominalSupport(,)$fNominalSupport()$fNominalSupport[]$fNominalSupportLiteral$fNominalSupportBasic$fNominalSupportOrdering$fNominalSupportFloat$fNominalSupportDouble$fNominalSupportChar$fNominalSupportInt$fNominalSupportInteger$fNominalSupportBool$fNominalSupportAtom $fShowLiteral $fEqAvoidee $fOrdAvoidee $fShowAvoidee GBindablegbindingNoBindBindablebindingBind NominalBinder BindAtomListBindNilBindCons:. atomlist_abst atomlist_openatomlist_open_for_printingatomlist_merge nobinding atom_binding binder_map binder_app.abstopenopen_for_printing basic_binding binder_gpair∘$fApplicativeNominalBinder$fFunctorNominalBinder$fEqBind $fGBindableM1$fGBindable:+:$fGBindable:*: $fGBindableU1 $fGBindableV1 $fGBindableK1$fBindableEither$fBindableMaybe$fBindable(,,,,,,)$fBindable(,,,,,)$fBindable(,,,,)$fBindable(,,,)$fBindable(,,) $fBindable(,) $fBindable() $fBindable[]$fBindableNoBind$fBindableLiteral$fBindableBasic$fBindableOrdering$fBindableFloat$fBindableDouble$fBindableChar $fBindableInt$fBindableInteger$fBindableBool$fBindableAtom$fNominalSupportBind $fNominalBind$fGenericBindAtomList$fNominalBindAtomList $fShowNoBind $fEqNoBind $fOrdNoBind$fGenericNoBind$fNominalNoBind$fNominalSupportNoBind AtomOfKindAtomKindsuggested_namesAtomicto_atom from_atomnames atomic_showwith_fresh_namedwith_fresh_namelistfresh fresh_namedfresh_namelist bind_named bind_namelist to_bindatom from_bindatommergeatomofkind_names $fAtomicAtom$fAtomicAtomOfKind$fNominalSupportAtomOfKind$fNominalAtomOfKind$fShowAtomOfKind$fEqAtomOfKind$fOrdAtomOfKind$fGenericAtomOfKind$fBindableAtomOfKind GNominalShow gshowsPrecSup isNullary SeparatorRecTupInfPre NominalShow showsPrecSupnominal_showList nominal_shownominal_showsPrecbasic_showsPrecSup$fGNominalShowM1$fGNominalShowM10$fGNominalShowM11$fGNominalShow:+:$fGNominalShow:*:$fGNominalShowU1$fGNominalShowV1$fGNominalShowK1 $fShowBind$fNominalShowSet$fNominalShowMap$fNominalShowBind$fNominalShowAtomOfKind$fNominalShowDefer$fNominalShow[]$fNominalShowEither$fNominalShowMaybe$fNominalShow(,,,,,,)$fNominalShow(,,,,,)$fNominalShow(,,,,)$fNominalShow(,,,)$fNominalShow(,,)$fNominalShow(,)$fNominalShow()$fNominalShowLiteral$fNominalShowBasic$fNominalShowOrdering$fNominalShowFloat$fNominalShowDouble$fNominalShowChar$fNominalShowInt$fNominalShowInteger$fNominalShowBool$fNominalShowAtom GHC.IO.UnsafeunsafePerformIO Data.Unique newUniqueghc-prim GHC.TypesIO GHC.ClassesOrd integer-gmpGHC.Integer.TypeIntegerBoolCharIntDoubleFloatOrderingGHC.BaseString ApplicativeNothingGHC.ShowShow showsPrecshowshowList