h&K>!      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                                                                                                            Safe689:; latticesHeyting algebra expression.Note: this type doesn't have  instance, as its  and  are structural.latticesDecide whether x ::  a is provable.Note:; this doesn't construct a proof term, but merely returns a .654<(C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus#BSD-3-Clause (see the file LICENSE)"Oleg Grenrus Safe latticesA partial ordering on sets ( 2http://en.wikipedia.org/wiki/Partially_ordered_set-) is a set equipped with a binary relation, , that obeys the following laws Reflexive: a  a Antisymmetric: a  b && b  a ==> a == b Transitive: a  b && b  c ==> a  c 'Two elements of the set are said to be 0 when they are are ordered with respect to the  relation. So  a b ==> a  b || b  a If ' always returns true then the relation # defines a total ordering (and an  instance may be defined). Any ' instance is trivially an instance of . + provides a convenient wrapper to satisfy  given .As an example consider the partial ordering on sets induced by set inclusion. Then for sets a and b, a  b  is true when a is a subset of b. Two sets are - if one is a subset of the other. Concretely *a = {1, 2, 3} b = {1, 3, 4} c = {1, 2} a  a =  a  b =  a  c =  b  a =  b  b =  b  c =  c  a =  c  b =  c  c =   a b =   a c =   b c =  lattices.The relation that induces the partial orderinglatticesWhether two elements are ordered with respect to the relation. A default implementation is given by  x y =  x y   y x latticesThe equality relation induced by the partial-order structure. It satisfies the laws of an equivalence relation:  Reflexive: a == a Symmetric: a == b ==> b == a Transitive: a == b && b == c ==> a == c !latticesLeast point of a partially ordered monotone function. Checks that the function is monotone."latticesLeast point of a partially ordered monotone function. Does not checks that the function is monotone.#latticesGreatest fixed point of a partially ordered antinone function. Checks that the function is antinone.$latticesGreatest fixed point of a partially ordered antinone function. Does not check that the function is antinone.%lattices Ordinal sum.-lattices = .1lattices !"#$ !"#$<(C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus#BSD-3-Clause (see the file LICENSE)"Oleg Grenrus Safe/6;!g3latticesMonoid wrapper for meet->6latticesMonoid wrapper for join->:lattices,A meet-semilattice with an identity element ; for @.Laws x @ ; D x  Corollary x ? ; DO identity O (x ? ;) @ ; DO absorption O ; <lattices,A join-semilattice with an identity element = for ?.Laws x ? = D x  Corollary x @ = DO identity O (x @ =) ? = DO absorption O = >lattices,An algebraic structure with joins and meets.See  ,http://en.wikipedia.org/wiki/Lattice_(order) and  +http://en.wikipedia.org/wiki/Absorption_law.>0 is very symmetric, which is seen from the laws: Associativity x ? (y ? z) D (x ? y) ? z x @ (y @ z) D (x @ y) @ z  Commutativity x ? y D y ? x x @ y D y @ x  Idempotency x ? x D x x @ x D x  Absorption a ? (a @ b) D a a @ (a ? b) D a ?latticesjoin@latticesmeetAlattices>The partial ordering induced by the join-semilattice structureClattices/The join of a list of join-semilattice elementsDlatticesThe join of at a list of join-semilattice elements (of length at least one)Elattices/The meet of a list of meet-semilattice elementsFlatticesThe meet of at a list of meet-semilattice elements (of length at least one)Glattices to ; and  to =Hlattices-Implementation of Kleene fixed-point theorem  7http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem. Assumes that the function is monotone and does not check if that is correct.Ilattices-Implementation of Kleene fixed-point theorem  7http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem&. Forces the function to be monotone.Jlattices-Implementation of Kleene fixed-point theorem  7http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem&. Forces the function to be monotone.Klattices-Implementation of Kleene fixed-point theorem  7http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem. Assumes that the function is antinone and does not check if that is correct.Llattices-Implementation of Kleene fixed-point theorem  7http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem&. Forces the function to be antinone.Mlattices-Implementation of Kleene fixed-point theorem  7http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem&. Forces the function to be antinone.NlatticesYlattices Ordinal sum.clatticesmlatticeswlatticeslattices3456789:;<=>@?ABCDEFGHIJKLM>@?ADBF<=:;CEG9345678IJHLMK?5@6<(C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus#BSD-3-Clause (see the file LICENSE)"Oleg Grenrus Safe689:;#zlattices4Graft a distinct top and bottom onto any type. The  is identity for @ and the absorbing element for ?. The  is the identity for ?# and and the absorbing element for @. Two + values join to top, unless they are equal. wide.png<(C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus#BSD-3-Clause (see the file LICENSE)"Oleg Grenrus Safe689:;$latticesThe opposite lattice of a given lattice. That is, switch meets and joins.(C) 2019 Oleg Grenrus#BSD-3-Clause (see the file LICENSE)"Oleg Grenrus Safe6;%tlatticesN_59, is smallest non-modular (and non-distributive) lattice. n5.png(C) 2019 Oleg Grenrus#BSD-3-Clause (see the file LICENSE)"Oleg Grenrus Safe6;&]latticesM_34, is smallest non-distributive, yet modular lattice. m3.png<(C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus#BSD-3-Clause (see the file LICENSE)"Oleg Grenrus Safe 689:;(8latticesGraft a distinct bottom onto an otherwise unbounded lattice. As a bonus, the bottom will be an absorbing element for the meet.lattices Interpret  a using the < of a.lattices Similar to  , but for  type. <(C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus#BSD-3-Clause (see the file LICENSE)"Oleg Grenrus Safe 689:;+latticesA pair lattice with a lexicographic ordering. This means in a join the second component of the resulting pair is the second component of the pair with the larger first component. If the first components are equal, then the second components will be joined. The meet is similar only it prefers the smaller first component.An application of this type is versioning. For example, a Last-Writer-Wins register would look like  ( Timestamp) v where the lattice structure handles the, presumably rare, case of matching  Timestamps. Typically this is done in an arbitary, but deterministic manner. <(C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus#BSD-3-Clause (see the file LICENSE)"Oleg Grenrus Safe 689:;-blatticesGraft a distinct top and bottom onto an otherwise unbounded lattice. The top is the absorbing element for the join, and the bottom is the absorbing element for the meet.lattices Interpret  a using the 9 of a.latticesFold . #BSD-3-Clause (see the file LICENSE)"Oleg Grenrus Safe/- Safe689:;0platticesFree distributive lattice. and  instances aren't structural.7(Var 'x' /\ Var 'y') == (Var 'y' /\ Var 'x' /\ Var 'x')TrueVar 'x' == Var 'y'FalseThis is  distributive lattice.5import Algebra.Lattice.M3 -- non distributive latticelet x = M3a; y = M3b; z = M3c#let lhs = Var x \/ (Var y /\ Var z).let rhs = (Var x \/ Var y) /\ (Var x \/ Var z) is distributive so lhs == rhsTrue&but when retracted, values are inequal"retractFree lhs == retractFree rhsFalse"(retractFree lhs, retractFree rhs) (M3a,M3i)  65 <(C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus#BSD-3-Clause (see the file LICENSE)"Oleg Grenrus Safe 689:;2_latticesGraft a distinct top onto an otherwise unbounded lattice. As a bonus, the top will be an absorbing element for the join.lattices Interpret  a using the : of a.lattices Similar to  , but for  type.<(C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus#BSD-3-Clause (see the file LICENSE)"Oleg Grenrus Safe 689:;3{latticesA divisibility lattice. join = , meet = .(C) 2019 Oleg Grenrus#BSD-3-Clause (see the file LICENSE)"Oleg Grenrus Safe/5latticesA Heyting algebra is a bounded lattice equipped with a binary operation a \to b of implication.Laws x  x D ; x @ (x  y) D x @ y y @ (x  y) D y x  (y @ z) D (x  y) @ (x  z) lattices Implication.lattices Negation.  x = x  = lattices Equivalence. x  y = (x  y) @ (y  x) lattices55(C) 2019 Oleg Grenrus#BSD-3-Clause (see the file LICENSE)"Oleg Grenrus Safe6;7glatticesThe simplest Heyting algebra that is not already a Boolean algebra is the totally ordered set \{ 0, \frac{1}{2}, 1 \}.lattices Not boolean:   ?  =  /=  Safe-Inferred8MlatticesMeet, alias for @.latticesJoin, alias for ?.latticesImplication, alias for .latticesEquivalence, alias for .6544<(C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus#BSD-3-Clause (see the file LICENSE)"Oleg Grenrus Safe 689:;:Glattices0A total order gives rise to a lattice. Join is  , meet is .latticesThis is interesting logic, as it satisfies both de Morgan laws; but isn't Boolean: i.e. law of exluded middle doesn't hold.Negation "smashes" value into  or .(C) 2019 Oleg Grenrus#BSD-3-Clause (see the file LICENSE)"Oleg Grenrus Safe6;;=latticesM_2 is isomorphic to \mathcal{P}\{\mathbb{B}\}, i.e. powerset of . m2.pngSafe689:;=latticesFree Heyting algebra.Note:  and  instances aren't structural.Top == (Var 'x' ==> Var 'x')TrueVar 'x' == Var 'y'FalseYou can test for taulogogies:leq Top $ (Var 'A' /\ Var 'B' ==> Var 'C') <=> (Var 'A' ==> Var 'B' ==> Var 'C')True/leq Top $ (Var 'A' /\ neg (Var 'A')) <=> BottomTrue,leq Top $ (Var 'A' \/ neg (Var 'A')) <=> TopFalse  6547(C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus#BSD-3-Clause (see the file LICENSE)"Oleg Grenrus Safe>lattices Eq (k -> v) is from  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOOPQQRSTUVWXYZ[\]^_`abc=de?fghijklmnopqrstuvwxyz{|}~                                                                              !                                               !"#lattices-2.2-ExsECSVnOmtEcARHt0JtvlAlgebra.Heyting.Free.ExprAlgebra.PartialOrdAlgebra.LatticeAlgebra.Lattice.WideAlgebra.Lattice.OpAlgebra.Lattice.N5Algebra.Lattice.M3Algebra.Lattice.LiftedAlgebra.Lattice.LexicographicAlgebra.Lattice.LevitatedAlgebra.Lattice.Free.FinalAlgebra.Lattice.FreeAlgebra.Lattice.DroppedAlgebra.Lattice.DivisibilityAlgebra.HeytingAlgebra.Lattice.ZeroHalfOneAlgebra.Lattice.UnicodeAlgebra.Lattice.OrderedAlgebra.Lattice.M2Algebra.Heyting.FreeAlgebra.PartialOrd.InstancesHeytingOrdered Data.List isSequenceOfData.Universe.InstancesEqExprVarBottomTop:/\::\/::=>: proofSearch $fMonadExpr$fApplicativeExpr $fShowCtx $fEqImplImpl $fOrdImplImpl$fShowImplImpl $fEqAtomImpl $fOrdAtomImpl$fShowAtomImpl$fEqAm$fOrdAm$fShowAm$fEqExpr $fOrdExpr $fShowExpr $fFunctorExpr$fFoldableExpr$fTraversableExpr $fGenericExpr$fGeneric1TYPEExpr $fDataExpr PartialOrdleq comparable partialOrdEqlfpFrom unsafeLfpFromgfpFrom unsafeGfpFrom$fPartialOrdEither$fPartialOrd(,)$fPartialOrdHashMap$fPartialOrdIntMap$fPartialOrdMap$fPartialOrdHashSet$fPartialOrdIntSet$fPartialOrdSet$fPartialOrd[]$fPartialOrdVoid$fPartialOrdAll$fPartialOrdAny$fPartialOrdBool$fPartialOrd()MeetgetMeetJoingetJoinBoundedLatticeBoundedMeetSemiLatticetopBoundedJoinSemiLatticebottomLattice\//\joinLeqmeetLeqjoinsjoins1meetsmeets1fromBool unsafeLfplfp unsafeGfpgfp $fLatticeSolo$fLatticeProperty $fLatticeVoid$fLatticeConst$fLatticeIdentity$fLatticeProxy$fLatticeTagged $fLatticeEndo $fLatticeAny $fLatticeAll $fLatticeBool$fLatticeEither $fLattice(,) $fLattice() $fLatticeFUN$fLatticeHashMap$fLatticeIntMap $fLatticeMap$fLatticeHashSet$fLatticeIntSet $fLatticeSet$fBoundedJoinSemiLatticeSolo $fBoundedJoinSemiLatticeProperty$fBoundedJoinSemiLatticeConst $fBoundedJoinSemiLatticeIdentity$fBoundedJoinSemiLatticeProxy$fBoundedJoinSemiLatticeTagged$fBoundedJoinSemiLatticeEndo$fBoundedJoinSemiLatticeAny$fBoundedJoinSemiLatticeAll$fBoundedJoinSemiLatticeBool$fBoundedJoinSemiLatticeEither$fBoundedJoinSemiLattice(,)$fBoundedJoinSemiLattice()$fBoundedJoinSemiLatticeFUN$fBoundedJoinSemiLatticeHashMap$fBoundedJoinSemiLatticeIntMap$fBoundedJoinSemiLatticeMap$fBoundedJoinSemiLatticeHashSet$fBoundedJoinSemiLatticeIntSet$fBoundedJoinSemiLatticeSet$fBoundedMeetSemiLatticeSolo $fBoundedMeetSemiLatticeProperty$fBoundedMeetSemiLatticeConst $fBoundedMeetSemiLatticeIdentity$fBoundedMeetSemiLatticeProxy$fBoundedMeetSemiLatticeTagged$fBoundedMeetSemiLatticeEndo$fBoundedMeetSemiLatticeAny$fBoundedMeetSemiLatticeAll$fBoundedMeetSemiLatticeBool$fBoundedMeetSemiLatticeEither$fBoundedMeetSemiLattice(,)$fBoundedMeetSemiLattice()$fBoundedMeetSemiLatticeFUN$fBoundedMeetSemiLatticeHashMap$fBoundedMeetSemiLatticeMap$fBoundedMeetSemiLatticeHashSet$fBoundedMeetSemiLatticeSet $fFiniteJoin$fUniverseJoin$fMonadZipJoin $fMonadJoin$fApplicativeJoin $fFunctorJoin$fPartialOrdJoin $fMonoidJoin$fSemigroupJoin $fFiniteMeet$fUniverseMeet$fMonadZipMeet $fMonadMeet$fApplicativeMeet $fFunctorMeet$fPartialOrdMeet $fMonoidMeet$fSemigroupMeet$fEqMeet $fOrdMeet $fReadMeet $fShowMeet $fBoundedMeet $fDataMeet $fGenericMeet$fEqJoin $fOrdJoin $fReadJoin $fShowJoin $fBoundedJoin $fDataJoin $fGenericJoinWideMiddle$fFunctionWide$fCoArbitraryWide$fArbitraryWide $fFiniteWide$fUniverseWide$fPartialOrdWide$fBoundedMeetSemiLatticeWide$fBoundedJoinSemiLatticeWide $fLatticeWide$fHashableWide $fNFDataWide $fMonadWide$fApplicativeWide$fEqWide $fOrdWide $fShowWide $fReadWide $fDataWide $fGenericWide $fFunctorWide$fFoldableWide$fTraversableWide$fGeneric1TYPEWideOpgetOp $fFunctionOp$fCoArbitraryOp $fArbitraryOp $fFiniteOp $fUniverseOp$fPartialOrdOp$fBoundedMeetSemiLatticeOp$fBoundedJoinSemiLatticeOp $fLatticeOp $fHashableOp $fNFDataOp $fMonadOp$fApplicativeOp$fOrdOp$fEqOp$fShowOp$fReadOp$fDataOp $fGenericOp $fFunctorOp $fFoldableOp$fTraversableOp$fGeneric1TYPEOpN5N5oN5aN5bN5cN5i $fHashableN5 $fNFDataN5 $fFiniteN5 $fUniverseN5 $fFunctionN5$fCoArbitraryN5 $fArbitraryN5$fBoundedMeetSemiLatticeN5$fBoundedJoinSemiLatticeN5 $fLatticeN5$fPartialOrdN5$fEqN5$fOrdN5$fReadN5$fShowN5$fEnumN5 $fBoundedN5$fDataN5 $fGenericN5M3M3oM3aM3bM3cM3i $fHashableM3 $fNFDataM3 $fFiniteM3 $fUniverseM3 $fFunctionM3$fCoArbitraryM3 $fArbitraryM3$fBoundedMeetSemiLatticeM3$fBoundedJoinSemiLatticeM3 $fLatticeM3$fPartialOrdM3$fEqM3$fOrdM3$fReadM3$fShowM3$fEnumM3 $fBoundedM3$fDataM3 $fGenericM3LiftedLift retractLifted foldLifted$fFunctionLifted$fCoArbitraryLifted$fArbitraryLifted$fFiniteLifted$fUniverseLifted$fBoundedMeetSemiLatticeLifted$fBoundedJoinSemiLatticeLifted$fLatticeLifted$fPartialOrdLifted$fHashableLifted$fNFDataLifted $fMonadLifted$fApplicativeLifted $fEqLifted $fOrdLifted $fShowLifted $fReadLifted $fDataLifted$fGenericLifted$fFunctorLifted$fFoldableLifted$fTraversableLifted$fGeneric1TYPELifted Lexicographic$fFunctionLexicographic$fCoArbitraryLexicographic$fArbitraryLexicographic$fFiniteLexicographic$fUniverseLexicographic$fPartialOrdLexicographic%$fBoundedMeetSemiLatticeLexicographic%$fBoundedJoinSemiLatticeLexicographic$fLatticeLexicographic$fHashableLexicographic$fNFDataLexicographic$fMonadLexicographic$fApplicativeLexicographic$fEqLexicographic$fOrdLexicographic$fShowLexicographic$fReadLexicographic$fDataLexicographic$fGenericLexicographic$fFunctorLexicographic$fFoldableLexicographic$fTraversableLexicographic$fGeneric1TYPELexicographic LevitatedLevitateretractLevitated foldLevitated$fFunctionLevitated$fCoArbitraryLevitated$fArbitraryLevitated$fFiniteLevitated$fUniverseLevitated!$fBoundedMeetSemiLatticeLevitated!$fBoundedJoinSemiLatticeLevitated$fLatticeLevitated$fPartialOrdLevitated$fHashableLevitated$fNFDataLevitated$fMonadLevitated$fApplicativeLevitated $fEqLevitated$fOrdLevitated$fShowLevitated$fReadLevitated$fDataLevitated$fGenericLevitated$fFunctorLevitated$fFoldableLevitated$fTraversableLevitated$fGeneric1TYPELevitatedFBoundedLatticelowerFBoundedLatticeFLattice lowerFLattice liftFLatticeretractFLatticeliftFBoundedLatticeretractFBoundedLattice$fFiniteFLattice$fUniverseFLattice $fBoundedMeetSemiLatticeFLattice $fBoundedJoinSemiLatticeFLattice$fLatticeFLattice$fFunctorFLattice$fFiniteFBoundedLattice$fUniverseFBoundedLattice'$fBoundedMeetSemiLatticeFBoundedLattice'$fBoundedJoinSemiLatticeFBoundedLattice$fLatticeFBoundedLattice$fFunctorFBoundedLatticeFreeliftFree retractFree substFree lowerFreetoExpr$fArbitraryFree$fPartialOrdFree$fEqFree $fLatticeFree $fMonadFree$fApplicativeFree $fShowFree $fFunctorFree$fFoldableFree$fTraversableFree $fGenericFree$fGeneric1TYPEFree $fDataFreeDroppedDropretractDropped foldDropped$fFunctionDropped$fCoArbitraryDropped$fArbitraryDropped$fFiniteDropped$fUniverseDropped$fBoundedMeetSemiLatticeDropped$fBoundedJoinSemiLatticeDropped$fLatticeDropped$fPartialOrdDropped$fHashableDropped$fNFDataDropped$fMonadDropped$fApplicativeDropped $fEqDropped $fOrdDropped $fShowDropped $fReadDropped $fDataDropped$fGenericDropped$fFunctorDropped$fFoldableDropped$fTraversableDropped$fGeneric1TYPEDropped DivisibilitygetDivisibility$fFunctionDivisibility$fCoArbitraryDivisibility$fArbitraryDivisibility$fFiniteDivisibility$fUniverseDivisibility$fPartialOrdDivisibility$$fBoundedJoinSemiLatticeDivisibility$fLatticeDivisibility$fHashableDivisibility$fNFDataDivisibility$fMonadDivisibility$fApplicativeDivisibility$fEqDivisibility$fOrdDivisibility$fShowDivisibility$fReadDivisibility$fDataDivisibility$fGenericDivisibility$fFunctorDivisibility$fFoldableDivisibility$fTraversableDivisibility$fGeneric1TYPEDivisibility==>neg<=>$fHeytingHashSet $fHeytingSet $fHeytingSolo$fHeytingConst$fHeytingTagged$fHeytingIdentity$fHeytingProxy $fHeytingEndo $fHeytingAny $fHeytingAll $fHeytingFUN $fHeytingBool $fHeyting() ZeroHalfOneZeroHalfOne$fHashableZeroHalfOne$fNFDataZeroHalfOne$fFiniteZeroHalfOne$fUniverseZeroHalfOne$fFunctionZeroHalfOne$fCoArbitraryZeroHalfOne$fArbitraryZeroHalfOne$fHeytingZeroHalfOne#$fBoundedMeetSemiLatticeZeroHalfOne#$fBoundedJoinSemiLatticeZeroHalfOne$fLatticeZeroHalfOne$fPartialOrdZeroHalfOne$fEqZeroHalfOne$fOrdZeroHalfOne$fReadZeroHalfOne$fShowZeroHalfOne$fEnumZeroHalfOne$fBoundedZeroHalfOne$fDataZeroHalfOne$fGenericZeroHalfOne∧∨⟹⟺ getOrdered$fFunctionOrdered$fCoArbitraryOrdered$fArbitraryOrdered$fFiniteOrdered$fUniverseOrdered$fPartialOrdOrdered$fHeytingOrdered$fBoundedMeetSemiLatticeOrdered$fBoundedJoinSemiLatticeOrdered$fLatticeOrdered$fHashableOrdered$fNFDataOrdered$fMonadOrdered$fApplicativeOrdered $fEqOrdered $fOrdOrdered $fShowOrdered $fReadOrdered $fDataOrdered$fGenericOrdered$fFunctorOrdered$fFoldableOrdered$fTraversableOrdered$fGeneric1TYPEOrderedM2M2oM2aM2bM2i toSetBool fromSetBool $fHashableM2 $fNFDataM2 $fFiniteM2 $fUniverseM2 $fFunctionM2$fCoArbitraryM2 $fArbitraryM2 $fHeytingM2$fBoundedMeetSemiLatticeM2$fBoundedJoinSemiLatticeM2 $fLatticeM2$fPartialOrdM2$fEqM2$fOrdM2$fReadM2$fShowM2$fEnumM2 $fBoundedM2$fDataM2 $fGenericM2 $fHeytingFree$fBoundedMeetSemiLatticeFree$fBoundedJoinSemiLatticeFree$fPartialOrdEndo$fPartialOrdFUNghc-prim GHC.ClassesOrd GHC.TypesBoolTrueFalse||base Data.MaybemaybeGHC.ReallcmgcdmaxminGHC.EnumminBoundmaxBound