kFu      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ non-portable experimentalwren@community.haskell.orgSafe<Compose comparison relations. Perform the first comparison,  and if it'3s not definitive, then fall through to perform the  second comparison.   non-portable experimentalwren@community.haskell.org TrustworthyChoose the smaller of x and y according to the order r. Choose the larger of x and y according to the order r.  Assert that x < y. This is just a shorthand for x <= pred y.  Assert that x <= y&. This is a popular constraint, so we 1 implement it specially. We could have said that  Add n x y =>  NatLE x y2, but the following inductive definition is a bit  more optimal. $Assert that the comparison relation r (LT_, EQ_, or  GT_) holds between x and y!; by structural induction on the & first, and then the second argument. 5The addition relation with full dependencies. Modes:  Add x y (x+y) & Add x (z-x) z -- when it's defined. & Add (z-y) y z -- when it's defined. <The primitive addition relation; by structural induction on  the first argument. Modes:  Add_ x y (x+y) ' Add_ x (z-x) z -- when it's defined. Assert  10*x + d == y where d is a decimal digit and both x  and y are decimal numbers. x may be zero. Essentially, this , is the general, non-structural, constructor/deconstructor of a , decimal number. This is like the assertion x:.d ~ y except that  we trim leading zeros of y in order to ensure that it is  well-formed.  The successor/.predecessor relation; by structural induction  on the first argument. Modes: > Succ x (succ x) -- i.e., given x, return the successor of x @ Succ (pred y) y -- i.e., given y, return the predecessor of y Is n a well-formed type of kind NatNE0? The only well-formed  types of kind NatNE0' are the non-zero well-formed types of  kind Nat6;, i.e., the type-level whole numbers in structurally  little-endian decimal. The hidden type class  (NatNE0_ n) entails (Nat_ n) and  (Reifies n Integer). Is n a well-formed type of kind Nat? The only well-formed  types of kind Nat0 are type-level natural numbers in structurally  little-endian decimal. The hidden type class (Nat_ n) entails (Reifies n Integer). <The connective. This should only be used left associatively ; (it associates to the left naturally). Decimal digits are & lexicographically big-endian, so they're written as usual;  however, they'.re structurally little-endian due to the left  associativity.  The digit 9.  The digit 8.  The digit 7.  The digit 6.  The digit 5.  The digit 4.  The digit 3.  The digit 2.  The digit 1.  The digit 0.  Return a 1 for the floor of the input divided by 10. Using  div10 n differs from using n `div` nat10 in that we take the ? floor of the result rather than being ill-typed; also in that  div10 isn'#t defined on single-digit numbers. * N.B., this will be ill-typed if x is greater than z. + N.B., this will be ill-typed if x is greater than z. - N.B., this will be ill-typed if x is greater than y. .Choose the larger of x and y. /Choose the smaller of x and y.   !"#$%&'()*+,-./      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[0  !"#$%&'()*+,-./0 !"#$%& '()*+,-/.  !"#$%&'()*+,-./      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[ non-portable experimentalwren@community.haskell.org Trustworthy0A finite set of integers Fin n = { i :: Int8 | 0 <= i < n } A with the usual ordering. This is typed as if using the standard  GADT presentation of Fin n%, however it is actually implemented  by a plain \. ] Often, we don't want to use the Fin n as a proxy, since that C would introduce spurious data dependencies. This function ignores ? its argument (other than for type propagation) so, hopefully, = via massive inlining this function will avoid that spurious  dependency. Hopefully... 'Also, this lets us minimize the use of -XScopedTypeVariables B which makes the Haddocks ugly. And so it lets us avoid the hacks  to hide our use of -XScopedTypeVariables. ,TODO: is this enough to ensure reflection is/can-be done at compile-time? > TODO: is there any way to tell GHC that this function should never& appear in the output of compilation? 1Like ^1, except it shows the type itself instead of the  value. 2Like _1, except it shows the type itself instead of the  value. 3 Return the ` of Fin n as a plain integer. This is 0 always zero, but is provided for symmetry with 4. 4 Return the a of Fin n as a plain integer. This is  always n-1, but it'(s helpful because you may not know what  n is at the time. b A version of c* which checks that the second argument is A in fact valid for its type before returning the first argument.  Throws an exception if the Fin n is invalid. The name and / argument ordering are indended for infix use. 5Extract the value of a Fin n. N.B., if somehow the Fin n" value was constructed invalidly, B then this function will throw an exception. However, this should  never7 happen. If it does, contact the maintainer since this  indicates a bug/insecurity in this library. 6Safely embed a number into Fin n. Use of this function will ? generally require an explicit type signature in order to know  which n to use. 7Safely embed a number into Fin n. This variant of 6 5 uses a proxy to avoid the need for type signatures. 8Safely embed integers into Fin n, where n is the first ? argument. We use rank-2 polymorphism to render the type-level  n= existentially quantified, thereby hiding the dependent type  from the compiler. However, n! will in fact be a skolem, so we  can'+t provide the continuation with proof that Nat n --- 7 unfortunately, rendering this function of little use.  toFinCPS n k i = | 0 <= i && i < n = Just (k i) -- morally speaking... " | otherwise = Nothing 9@The maximum-element view. This strengthens the type by removing  the maximum element:   maxView maxBound = Nothing 3 maxView x = Just x -- morally speaking... !The opposite of this function is ;. ) maxView . weaken == Just ' maybe maxBound weaken . maxView == id : A variant of 9( which allows strengthening the type by @ multiple steps. Use of this function will generally require an 0 explicit type signature in order to know which m to use. !The opposite of this function is <. When the choice of  m and n! is held constant, we have that: # maxViewLE . weakenLE == Just H fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) ;<Embed a finite domain into the next larger one, keeping the  same position relative to ` . That is,  ! fromFin (weaken x) == fromFin x !The opposite of this function is 9. ) maxView . weaken == Just ' maybe maxBound weaken . maxView == id < A variant of ;$ which allows weakening the type by @ multiple steps. Use of this function will generally require an 0 explicit type signature in order to know which n to use. !The opposite of this function is :. When the choice  of m and n! is held constant, we have that: # maxViewLE . weakenLE == Just H fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) =<The predecessor view. This strengthens the type by shifting  everything down by one:   predView 0 = Nothing 1 predView x = Just (x-1) -- morally speaking... !The opposite of this function is >. " predView . widen == Just  maybe 0 widen . predView == id ><Embed a finite domain into the next larger one, keeping the  same position relative to a. That is, we shift everything  up by one:  $ fromFin (widen x) == 1 + fromFin x !The opposite of this function is =. " predView . widen == Just  maybe 0 widen . predView == id ?<Embed a finite domain into any larger one, keeping the same  position relative to a . That is,  6 maxBoundOf y - fromFin y == maxBoundOf x - fromFin x  where y = widenLE x =Use of this function will generally require an explicit type " signature in order to know which n to use. @A type-signature variant of < because we cannot  automatically deduce that Add m n o ==> NatLE m o. This is the  left half of B. AA type-signature variant of ? because we cannot  automatically deduce that Add m n o ==> NatLE n o. This is the  right half of B. B;The ordinal-sum functor, on objects. This internalizes the  disjoint union, mapping  Fin m + Fin n into Fin(m+n) by > placing the image of the summands next to one another in the > codomain, thereby preserving the structure of both summands. CThe inverse of B. D>The ordinal-sum functor, on morphisms. If we view the maps as A bipartite graphs, then the new map is the result of placing the = left and right maps next to one another. This is similar to  (+++) from  Control.Arrow. EThe " face maps" for Fin" viewed as the standard simplices ? (aka: the thinning view). Traditionally spelled with delta or  epsilon. For each i+, it is the unique injective monotonic map  that skips i . That is,  F thin i = (\j -> if j < i then j else succ j) -- morally speaking... 1Which has the important universal property that:  thin i j /= i FThe "degeneracy maps" for Fin viewed as the standard > simplices. Traditionally spelled with sigma or eta. For each  i8, it is the unique surjective monotonic map that covers i  twice. That is,  H thick i = (\j -> if j <= i then j else pred j) -- morally speaking... 1Which has the important universal property that:  thick i (i+1) == i .0d]1234be56789:;<=>?@ABCDThe left morphism The right morphism EFfghijklmnopqrstuvwx0123456789:;<=>?@ABCDEF012346785;<@9:>?A=BCDEF-0d]1234be56789:;<=>?@ABCDEFfghijklmnopqrstuvwx non-portable experimentalwren@community.haskell.org TrustworthyGA finite set of integers Fin n = { i :: Int16 | 0 <= i < n } A with the usual ordering. This is typed as if using the standard  GADT presentation of Fin n%, however it is actually implemented  by a plain y. z Often, we don't want to use the Fin n as a proxy, since that C would introduce spurious data dependencies. This function ignores ? its argument (other than for type propagation) so, hopefully, = via massive inlining this function will avoid that spurious  dependency. Hopefully... 'Also, this lets us minimize the use of -XScopedTypeVariables B which makes the Haddocks ugly. And so it lets us avoid the hacks  to hide our use of -XScopedTypeVariables. ,TODO: is this enough to ensure reflection is/can-be done at compile-time? > TODO: is there any way to tell GHC that this function should never& appear in the output of compilation? HLike ^1, except it shows the type itself instead of the  value. ILike _1, except it shows the type itself instead of the  value. J Return the ` of Fin n as a plain integer. This is 0 always zero, but is provided for symmetry with K. K Return the a of Fin n as a plain integer. This is  always n-1, but it'(s helpful because you may not know what  n is at the time. { A version of c* which checks that the second argument is A in fact valid for its type before returning the first argument.  Throws an exception if the Fin n is invalid. The name and / argument ordering are indended for infix use. LExtract the value of a Fin n. N.B., if somehow the Fin n" value was constructed invalidly, B then this function will throw an exception. However, this should  never7 happen. If it does, contact the maintainer since this  indicates a bug/insecurity in this library. MSafely embed a number into Fin n. Use of this function will ? generally require an explicit type signature in order to know  which n to use. NSafely embed a number into Fin n. This variant of M 5 uses a proxy to avoid the need for type signatures. OSafely embed integers into Fin n, where n is the first ? argument. We use rank-2 polymorphism to render the type-level  n= existentially quantified, thereby hiding the dependent type  from the compiler. However, n! will in fact be a skolem, so we  can'+t provide the continuation with proof that Nat n --- 7 unfortunately, rendering this function of little use.  toFinCPS n k i = | 0 <= i && i < n = Just (k i) -- morally speaking... " | otherwise = Nothing P@The maximum-element view. This strengthens the type by removing  the maximum element:   maxView maxBound = Nothing 3 maxView x = Just x -- morally speaking... !The opposite of this function is R. ) maxView . weaken == Just ' maybe maxBound weaken . maxView == id Q A variant of P( which allows strengthening the type by @ multiple steps. Use of this function will generally require an 0 explicit type signature in order to know which m to use. !The opposite of this function is S. When the choice of  m and n! is held constant, we have that: # maxViewLE . weakenLE == Just H fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) R<Embed a finite domain into the next larger one, keeping the  same position relative to ` . That is,  ! fromFin (weaken x) == fromFin x !The opposite of this function is P. ) maxView . weaken == Just ' maybe maxBound weaken . maxView == id S A variant of R$ which allows weakening the type by @ multiple steps. Use of this function will generally require an 0 explicit type signature in order to know which n to use. !The opposite of this function is Q. When the choice  of m and n! is held constant, we have that: # maxViewLE . weakenLE == Just H fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) T<The predecessor view. This strengthens the type by shifting  everything down by one:   predView 0 = Nothing 1 predView x = Just (x-1) -- morally speaking... !The opposite of this function is U. " predView . widen == Just  maybe 0 widen . predView == id U<Embed a finite domain into the next larger one, keeping the  same position relative to a. That is, we shift everything  up by one:  $ fromFin (widen x) == 1 + fromFin x !The opposite of this function is T. " predView . widen == Just  maybe 0 widen . predView == id V<Embed a finite domain into any larger one, keeping the same  position relative to a . That is,  6 maxBoundOf y - fromFin y == maxBoundOf x - fromFin x  where y = widenLE x =Use of this function will generally require an explicit type " signature in order to know which n to use. WA type-signature variant of S because we cannot  automatically deduce that Add m n o ==> NatLE m o. This is the  left half of Y. XA type-signature variant of V because we cannot  automatically deduce that Add m n o ==> NatLE n o. This is the  right half of Y. Y;The ordinal-sum functor, on objects. This internalizes the  disjoint union, mapping  Fin m + Fin n into Fin(m+n) by > placing the image of the summands next to one another in the > codomain, thereby preserving the structure of both summands. ZThe inverse of Y. [>The ordinal-sum functor, on morphisms. If we view the maps as A bipartite graphs, then the new map is the result of placing the = left and right maps next to one another. This is similar to  (+++) from  Control.Arrow. \The " face maps" for Fin" viewed as the standard simplices ? (aka: the thinning view). Traditionally spelled with delta or  epsilon. For each i+, it is the unique injective monotonic map  that skips i . That is,  F thin i = (\j -> if j < i then j else succ j) -- morally speaking... 1Which has the important universal property that:  thin i j /= i ]The "degeneracy maps" for Fin viewed as the standard > simplices. Traditionally spelled with sigma or eta. For each  i8, it is the unique surjective monotonic map that covers i  twice. That is,  H thick i = (\j -> if j <= i then j else pred j) -- morally speaking... 1Which has the important universal property that:  thick i (i+1) == i .G|zHIJK{}LMNOPQRSTUVWXYZ[The left morphism The right morphism \]~GHIJKLMNOPQRSTUVWXYZ[\]GHIJKMNOLRSWPQUVXTYZ[\]-G|zHIJK{}LMNOPQRSTUVWXYZ[\]~ non-portable experimentalwren@community.haskell.org Trustworthy^A finite set of integers Fin n = { i :: Int32 | 0 <= i < n } A with the usual ordering. This is typed as if using the standard  GADT presentation of Fin n%, however it is actually implemented  by a plain .  Often, we don't want to use the Fin n as a proxy, since that C would introduce spurious data dependencies. This function ignores ? its argument (other than for type propagation) so, hopefully, = via massive inlining this function will avoid that spurious  dependency. Hopefully... 'Also, this lets us minimize the use of -XScopedTypeVariables B which makes the Haddocks ugly. And so it lets us avoid the hacks  to hide our use of -XScopedTypeVariables. ,TODO: is this enough to ensure reflection is/can-be done at compile-time? > TODO: is there any way to tell GHC that this function should never& appear in the output of compilation? _Like ^1, except it shows the type itself instead of the  value. `Like _1, except it shows the type itself instead of the  value. a Return the ` of Fin n as a plain integer. This is 0 always zero, but is provided for symmetry with b. b Return the a of Fin n as a plain integer. This is  always n-1, but it'(s helpful because you may not know what  n is at the time.  A version of c* which checks that the second argument is A in fact valid for its type before returning the first argument.  Throws an exception if the Fin n is invalid. The name and / argument ordering are indended for infix use. cExtract the value of a Fin n. N.B., if somehow the Fin n" value was constructed invalidly, B then this function will throw an exception. However, this should  never7 happen. If it does, contact the maintainer since this  indicates a bug/insecurity in this library. dSafely embed a number into Fin n. Use of this function will ? generally require an explicit type signature in order to know  which n to use. eSafely embed a number into Fin n. This variant of d 5 uses a proxy to avoid the need for type signatures. fSafely embed integers into Fin n, where n is the first ? argument. We use rank-2 polymorphism to render the type-level  n= existentially quantified, thereby hiding the dependent type  from the compiler. However, n! will in fact be a skolem, so we  can'+t provide the continuation with proof that Nat n --- 7 unfortunately, rendering this function of little use.  toFinCPS n k i = | 0 <= i && i < n = Just (k i) -- morally speaking... " | otherwise = Nothing g@The maximum-element view. This strengthens the type by removing  the maximum element:   maxView maxBound = Nothing 3 maxView x = Just x -- morally speaking... !The opposite of this function is i. ) maxView . weaken == Just ' maybe maxBound weaken . maxView == id h A variant of g( which allows strengthening the type by @ multiple steps. Use of this function will generally require an 0 explicit type signature in order to know which m to use. !The opposite of this function is j. When the choice of  m and n! is held constant, we have that: # maxViewLE . weakenLE == Just H fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) i<Embed a finite domain into the next larger one, keeping the  same position relative to ` . That is,  ! fromFin (weaken x) == fromFin x !The opposite of this function is g. ) maxView . weaken == Just ' maybe maxBound weaken . maxView == id j A variant of i$ which allows weakening the type by @ multiple steps. Use of this function will generally require an 0 explicit type signature in order to know which n to use. !The opposite of this function is h. When the choice  of m and n! is held constant, we have that: # maxViewLE . weakenLE == Just H fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) k<The predecessor view. This strengthens the type by shifting  everything down by one:   predView 0 = Nothing 1 predView x = Just (x-1) -- morally speaking... !The opposite of this function is l. " predView . widen == Just  maybe 0 widen . predView == id l<Embed a finite domain into the next larger one, keeping the  same position relative to a. That is, we shift everything  up by one:  $ fromFin (widen x) == 1 + fromFin x !The opposite of this function is k. " predView . widen == Just  maybe 0 widen . predView == id m<Embed a finite domain into any larger one, keeping the same  position relative to a . That is,  6 maxBoundOf y - fromFin y == maxBoundOf x - fromFin x  where y = widenLE x =Use of this function will generally require an explicit type " signature in order to know which n to use. nA type-signature variant of j because we cannot  automatically deduce that Add m n o ==> NatLE m o. This is the  left half of p. oA type-signature variant of m because we cannot  automatically deduce that Add m n o ==> NatLE n o. This is the  right half of p. p;The ordinal-sum functor, on objects. This internalizes the  disjoint union, mapping  Fin m + Fin n into Fin(m+n) by > placing the image of the summands next to one another in the > codomain, thereby preserving the structure of both summands. qThe inverse of p. r>The ordinal-sum functor, on morphisms. If we view the maps as A bipartite graphs, then the new map is the result of placing the = left and right maps next to one another. This is similar to  (+++) from  Control.Arrow. sThe " face maps" for Fin" viewed as the standard simplices ? (aka: the thinning view). Traditionally spelled with delta or  epsilon. For each i+, it is the unique injective monotonic map  that skips i . That is,  F thin i = (\j -> if j < i then j else succ j) -- morally speaking... 1Which has the important universal property that:  thin i j /= i tThe "degeneracy maps" for Fin viewed as the standard > simplices. Traditionally spelled with sigma or eta. For each  i8, it is the unique surjective monotonic map that covers i  twice. That is,  H thick i = (\j -> if j <= i then j else pred j) -- morally speaking... 1Which has the important universal property that:  thick i (i+1) == i .^_`abcdefghijklmnopqrThe left morphism The right morphism st^_`abcdefghijklmnopqrst^_`abdefcijnghlmokpqrst-^_`abcdefghijklmnopqrst non-portable experimentalwren@community.haskell.org TrustworthyuA finite set of integers Fin n = { i :: Int64 | 0 <= i < n } A with the usual ordering. This is typed as if using the standard  GADT presentation of Fin n%, however it is actually implemented  by a plain .  Often, we don't want to use the Fin n as a proxy, since that C would introduce spurious data dependencies. This function ignores ? its argument (other than for type propagation) so, hopefully, = via massive inlining this function will avoid that spurious  dependency. Hopefully... 'Also, this lets us minimize the use of -XScopedTypeVariables B which makes the Haddocks ugly. And so it lets us avoid the hacks  to hide our use of -XScopedTypeVariables. ,TODO: is this enough to ensure reflection is/can-be done at compile-time? > TODO: is there any way to tell GHC that this function should never& appear in the output of compilation? vLike ^1, except it shows the type itself instead of the  value. wLike _1, except it shows the type itself instead of the  value. x Return the ` of Fin n as a plain integer. This is 0 always zero, but is provided for symmetry with y. y Return the a of Fin n as a plain integer. This is  always n-1, but it'(s helpful because you may not know what  n is at the time.  A version of c* which checks that the second argument is A in fact valid for its type before returning the first argument.  Throws an exception if the Fin n is invalid. The name and / argument ordering are indended for infix use. zExtract the value of a Fin n. N.B., if somehow the Fin n" value was constructed invalidly, B then this function will throw an exception. However, this should  never7 happen. If it does, contact the maintainer since this  indicates a bug/insecurity in this library. {Safely embed a number into Fin n. Use of this function will ? generally require an explicit type signature in order to know  which n to use. |Safely embed a number into Fin n. This variant of { 5 uses a proxy to avoid the need for type signatures. }Safely embed integers into Fin n, where n is the first ? argument. We use rank-2 polymorphism to render the type-level  n= existentially quantified, thereby hiding the dependent type  from the compiler. However, n! will in fact be a skolem, so we  can'+t provide the continuation with proof that Nat n --- 7 unfortunately, rendering this function of little use.  toFinCPS n k i = | 0 <= i && i < n = Just (k i) -- morally speaking... " | otherwise = Nothing ~@The maximum-element view. This strengthens the type by removing  the maximum element:   maxView maxBound = Nothing 3 maxView x = Just x -- morally speaking... !The opposite of this function is . ) maxView . weaken == Just ' maybe maxBound weaken . maxView == id  A variant of ~( which allows strengthening the type by @ multiple steps. Use of this function will generally require an 0 explicit type signature in order to know which m to use. !The opposite of this function is . When the choice of  m and n! is held constant, we have that: # maxViewLE . weakenLE == Just H fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) <Embed a finite domain into the next larger one, keeping the  same position relative to ` . That is,  ! fromFin (weaken x) == fromFin x !The opposite of this function is ~. ) maxView . weaken == Just ' maybe maxBound weaken . maxView == id  A variant of $ which allows weakening the type by @ multiple steps. Use of this function will generally require an 0 explicit type signature in order to know which n to use. !The opposite of this function is . When the choice  of m and n! is held constant, we have that: # maxViewLE . weakenLE == Just H fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) <The predecessor view. This strengthens the type by shifting  everything down by one:   predView 0 = Nothing 1 predView x = Just (x-1) -- morally speaking... !The opposite of this function is . " predView . widen == Just  maybe 0 widen . predView == id <Embed a finite domain into the next larger one, keeping the  same position relative to a. That is, we shift everything  up by one:  $ fromFin (widen x) == 1 + fromFin x !The opposite of this function is . " predView . widen == Just  maybe 0 widen . predView == id <Embed a finite domain into any larger one, keeping the same  position relative to a . That is,  6 maxBoundOf y - fromFin y == maxBoundOf x - fromFin x  where y = widenLE x =Use of this function will generally require an explicit type " signature in order to know which n to use. A type-signature variant of  because we cannot  automatically deduce that Add m n o ==> NatLE m o. This is the  left half of . A type-signature variant of  because we cannot  automatically deduce that Add m n o ==> NatLE n o. This is the  right half of . ;The ordinal-sum functor, on objects. This internalizes the  disjoint union, mapping  Fin m + Fin n into Fin(m+n) by > placing the image of the summands next to one another in the > codomain, thereby preserving the structure of both summands. The inverse of . >The ordinal-sum functor, on morphisms. If we view the maps as A bipartite graphs, then the new map is the result of placing the = left and right maps next to one another. This is similar to  (+++) from  Control.Arrow. The " face maps" for Fin" viewed as the standard simplices ? (aka: the thinning view). Traditionally spelled with delta or  epsilon. For each i+, it is the unique injective monotonic map  that skips i . That is,  F thin i = (\j -> if j < i then j else succ j) -- morally speaking... 1Which has the important universal property that:  thin i j /= i The "degeneracy maps" for Fin viewed as the standard > simplices. Traditionally spelled with sigma or eta. For each  i8, it is the unique surjective monotonic map that covers i  twice. That is,  H thick i = (\j -> if j <= i then j else pred j) -- morally speaking... 1Which has the important universal property that:  thick i (i+1) == i .uvwxyz{|}~The left morphism The right morphism uvwxyz{|}~uvwxy{|}z~-uvwxyz{|}~ non-portable experimentalwren@community.haskell.org TrustworthyA finite set of integers Fin n = { i :: Integer | 0 <= i < n } A with the usual ordering. This is typed as if using the standard  GADT presentation of Fin n%, however it is actually implemented  by a plain . ?If you care more about performance than mathematical accuracy,  see Data.Number.Fin.Int32# for an alternative implementation  as a newtype of Int32(. Note, however, that doing so makes it = harder to reason about code since it introduces many corner  cases.  Often, we don't want to use the Fin n as a proxy, since that C would introduce spurious data dependencies. This function ignores ? its argument (other than for type propagation) so, hopefully, = via massive inlining this function will avoid that spurious  dependency. Hopefully... 'Also, this lets us minimize the use of -XScopedTypeVariables B which makes the Haddocks ugly. And so it lets us avoid the hacks  to hide our use of -XScopedTypeVariables. ,TODO: is this enough to ensure reflection is/can-be done at compile-time? > TODO: is there any way to tell GHC that this function should never& appear in the output of compilation? Like ^1, except it shows the type itself instead of the  value. Like _1, except it shows the type itself instead of the  value.  Return the ` of Fin n as a plain integer. This is 0 always zero, but is provided for symmetry with .  Return the a of Fin n as a plain integer. This is  always n-1, but it'(s helpful because you may not know what  n is at the time.  A version of c* which checks that the second argument is A in fact valid for its type before returning the first argument.  Throws an exception if the Fin n is invalid. The name and / argument ordering are indended for infix use. Extract the value of a Fin n. N.B., if somehow the Fin n" value was constructed invalidly, B then this function will throw an exception. However, this should  never7 happen. If it does, contact the maintainer since this  indicates a bug/insecurity in this library. Safely embed a number into Fin n. Use of this function will ? generally require an explicit type signature in order to know  which n to use. Safely embed a number into Fin n. This variant of  5 uses a proxy to avoid the need for type signatures. Safely embed integers into Fin n, where n is the first ? argument. We use rank-2 polymorphism to render the type-level  n= existentially quantified, thereby hiding the dependent type  from the compiler. However, n! will in fact be a skolem, so we  can'+t provide the continuation with proof that Nat n --- 7 unfortunately, rendering this function of little use.  toFinCPS n k i = | 0 <= i && i < n = Just (k i) -- morally speaking... " | otherwise = Nothing @The maximum-element view. This strengthens the type by removing  the maximum element:   maxView maxBound = Nothing 3 maxView x = Just x -- morally speaking... !The opposite of this function is . ) maxView . weaken == Just ' maybe maxBound weaken . maxView == id  A variant of ( which allows strengthening the type by @ multiple steps. Use of this function will generally require an 0 explicit type signature in order to know which m to use. !The opposite of this function is . When the choice of  m and n! is held constant, we have that: # maxViewLE . weakenLE == Just H fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) <Embed a finite domain into the next larger one, keeping the  same position relative to ` . That is,  ! fromFin (weaken x) == fromFin x !The opposite of this function is . ) maxView . weaken == Just ' maybe maxBound weaken . maxView == id  A variant of $ which allows weakening the type by @ multiple steps. Use of this function will generally require an 0 explicit type signature in order to know which n to use. !The opposite of this function is . When the choice  of m and n! is held constant, we have that: # maxViewLE . weakenLE == Just H fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing) <The predecessor view. This strengthens the type by shifting  everything down by one:   predView 0 = Nothing 1 predView x = Just (x-1) -- morally speaking... !The opposite of this function is . " predView . widen == Just  maybe 0 widen . predView == id <Embed a finite domain into the next larger one, keeping the  same position relative to a. That is, we shift everything  up by one:  $ fromFin (widen x) == 1 + fromFin x !The opposite of this function is . " predView . widen == Just  maybe 0 widen . predView == id <Embed a finite domain into any larger one, keeping the same  position relative to a . That is,  6 maxBoundOf y - fromFin y == maxBoundOf x - fromFin x  where y = widenLE x =Use of this function will generally require an explicit type " signature in order to know which n to use. A type-signature variant of  because we cannot  automatically deduce that Add m n o ==> NatLE m o. This is the  left half of . A type-signature variant of  because we cannot  automatically deduce that Add m n o ==> NatLE n o. This is the  right half of . ;The ordinal-sum functor, on objects. This internalizes the  disjoint union, mapping  Fin m + Fin n into Fin(m+n) by > placing the image of the summands next to one another in the > codomain, thereby preserving the structure of both summands. The inverse of . >The ordinal-sum functor, on morphisms. If we view the maps as A bipartite graphs, then the new map is the result of placing the = left and right maps next to one another. This is similar to  (+++) from  Control.Arrow. The " face maps" for Fin" viewed as the standard simplices ? (aka: the thinning view). Traditionally spelled with delta or  epsilon. For each i+, it is the unique injective monotonic map  that skips i . That is,  F thin i = (\j -> if j < i then j else succ j) -- morally speaking... 1Which has the important universal property that:  thin i j /= i The "degeneracy maps" for Fin viewed as the standard > simplices. Traditionally spelled with sigma or eta. For each  i8, it is the unique surjective monotonic map that covers i  twice. That is,  H thick i = (\j -> if j <= i then j else pred j) -- morally speaking... 1Which has the important universal property that:  thick i (i+1) == i .The left morphism The right morphism - non-portable experimentalwren@community.haskell.org Safe-Inferred      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNO9:;<=>?@ABCDEFGHIJKLMNO9:;<=>?@ABCDEFGHIJKLMNO9:;<=>?@ABCDEFGHIJKLMNO9:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~          9 !"#$%&'()*+  ,9 !"#$%&'()*+  -9 !"#$%&'()*+  .9 !"#$%&'()*+/019 !"#$%&'()*+2data-fin-0.1.0Data.Number.Fin.TyDecimalData.Number.Fin.Int8Data.Number.Fin.Int16Data.Number.Fin.Int32Data.Number.Fin.Int64Data.Number.Fin.IntegerData.Number.Fin.TyOrderingData.Number.FinGT_EQ_LT_NatLTNatLECompareAddSuccMaxBoundWord64MaxBoundWord32MaxBoundWord16 MaxBoundWord8 MaxBoundInt64 MaxBoundInt32 MaxBoundInt16 MaxBoundInt8NatNE0Nat:.D9D8D7D6D5D4D3D2D1D0nat0nat1nat2nat3nat4nat5nat6nat7nat8nat9succpredaddminussubtractcompare assert_NatLEmaxminFin showFinType showsFinType minBoundOf maxBoundOffromFintoFin toFinProxytoFinCPSmaxView maxViewLEweakenweakenLEpredViewwidenwidenLE weakenPlus widenPlusplusunplusfplusthinthickNCS $fNCSLT_rLT_ $fNCSGT_rGT_ $fNCSEQ_rr$fReifies*GT_Ordering$fReifies*EQ_Ordering$fReifies*LT_OrderingMin_Max_Add_Snocdiv10 tagged-0.6.1 Data.ProxyProxyNat_NatNE0_Digit_ $fMin_xyGT_y $fMin_xyEQ_x $fMin_xyLT_x $fMax_xyGT_x $fMax_xyEQ_y $fMax_xyLT_y $fNatLTxy $fNatLE:.:. $fNatLE:.:.0 $fNatLE:.:.1 $fNatLE:.:.2 $fNatLE:.:.3 $fNatLE:.:.4 $fNatLE:.:.5 $fNatLE:.:.6 $fNatLE:.:.7 $fNatLE:.:.8 $fNatLE:.:.9 $fNatLE:.:.10 $fNatLE:.:.11 $fNatLE:.:.12 $fNatLE:.:.13 $fNatLE:.:.14 $fNatLE:.:.15 $fNatLE:.:.16 $fNatLE:.:.17 $fNatLE:.:.18 $fNatLE:.:.19 $fNatLE:.:.20 $fNatLE:.:.21 $fNatLE:.:.22 $fNatLE:.:.23 $fNatLE:.:.24 $fNatLE:.:.25 $fNatLE:.:.26 $fNatLE:.:.27 $fNatLE:.:.28 $fNatLE:.:.29 $fNatLE:.:.30 $fNatLE:.:.31 $fNatLE:.:.32 $fNatLE:.:.33 $fNatLE:.:.34 $fNatLE:.:.35 $fNatLE:.:.36 $fNatLE:.:.37 $fNatLE:.:.38 $fNatLE:.:.39 $fNatLE:.:.40 $fNatLE:.:.41 $fNatLE:.:.42 $fNatLE:.:.43 $fNatLE:.:.44 $fNatLE:.:.45 $fNatLE:.:.46 $fNatLE:.:.47 $fNatLE:.:.48 $fNatLE:.:.49 $fNatLE:.:.50 $fNatLE:.:.51 $fNatLE:.:.52 $fNatLE:.:.53 $fNatLE:.:.54 $fNatLE:.:.55 $fNatLE:.:.56 $fNatLE:.:.57 $fNatLE:.:.58 $fNatLE:.:.59 $fNatLE:.:.60 $fNatLE:.:.61 $fNatLE:.:.62 $fNatLE:.:.63 $fNatLE:.:.64 $fNatLE:.:.65 $fNatLE:.:.66 $fNatLE:.:.67 $fNatLE:.:.68 $fNatLE:.:.69 $fNatLE:.:.70 $fNatLE:.:.71 $fNatLE:.:.72 $fNatLE:.:.73 $fNatLE:.:.74 $fNatLE:.:.75 $fNatLE:.:.76 $fNatLE:.:.77 $fNatLE:.:.78 $fNatLE:.:.79 $fNatLE:.:.80 $fNatLE:.:.81 $fNatLE:.:.82 $fNatLE:.:.83 $fNatLE:.:.84 $fNatLE:.:.85 $fNatLE:.:.86 $fNatLE:.:.87 $fNatLE:.:.88 $fNatLE:.:.89 $fNatLE:.:.90 $fNatLE:.:.91 $fNatLE:.:.92 $fNatLE:.:.93 $fNatLE:.:.94 $fNatLE:.:.95 $fNatLE:.:.96 $fNatLE:.:.97 $fNatLE:.:.98 $fNatLED9:. $fNatLED9D9 $fNatLED8:. $fNatLED8D9 $fNatLED8D8 $fNatLED7:. $fNatLED7D9 $fNatLED7D8 $fNatLED7D7 $fNatLED6:. $fNatLED6D9 $fNatLED6D8 $fNatLED6D7 $fNatLED6D6 $fNatLED5:. $fNatLED5D9 $fNatLED5D8 $fNatLED5D7 $fNatLED5D6 $fNatLED5D5 $fNatLED4:. $fNatLED4D9 $fNatLED4D8 $fNatLED4D7 $fNatLED4D6 $fNatLED4D5 $fNatLED4D4 $fNatLED3:. $fNatLED3D9 $fNatLED3D8 $fNatLED3D7 $fNatLED3D6 $fNatLED3D5 $fNatLED3D4 $fNatLED3D3 $fNatLED2:. $fNatLED2D9 $fNatLED2D8 $fNatLED2D7 $fNatLED2D6 $fNatLED2D5 $fNatLED2D4 $fNatLED2D3 $fNatLED2D2 $fNatLED1:. $fNatLED1D9 $fNatLED1D8 $fNatLED1D7 $fNatLED1D6 $fNatLED1D5 $fNatLED1D4 $fNatLED1D3 $fNatLED1D2 $fNatLED1D1 $fNatLED0:. $fNatLED0D9 $fNatLED0D8 $fNatLED0D7 $fNatLED0D6 $fNatLED0D5 $fNatLED0D4 $fNatLED0D3 $fNatLED0D2 $fNatLED0D1 $fNatLED0D0$fCompare:.:.r$fCompare:.D9GT_$fCompare:.D8GT_$fCompare:.D7GT_$fCompare:.D6GT_$fCompare:.D5GT_$fCompare:.D4GT_$fCompare:.D3GT_$fCompare:.D2GT_$fCompare:.D1GT_$fCompare:.D0GT_$fCompareD9:.LT_$fCompareD9D9EQ_$fCompareD9D8GT_$fCompareD9D7GT_$fCompareD9D6GT_$fCompareD9D5GT_$fCompareD9D4GT_$fCompareD9D3GT_$fCompareD9D2GT_$fCompareD9D1GT_$fCompareD9D0GT_$fCompareD8:.LT_$fCompareD8D9LT_$fCompareD8D8EQ_$fCompareD8D7GT_$fCompareD8D6GT_$fCompareD8D5GT_$fCompareD8D4GT_$fCompareD8D3GT_$fCompareD8D2GT_$fCompareD8D1GT_$fCompareD8D0GT_$fCompareD7:.LT_$fCompareD7D9LT_$fCompareD7D8LT_$fCompareD7D7EQ_$fCompareD7D6GT_$fCompareD7D5GT_$fCompareD7D4GT_$fCompareD7D3GT_$fCompareD7D2GT_$fCompareD7D1GT_$fCompareD7D0GT_$fCompareD6:.LT_$fCompareD6D9LT_$fCompareD6D8LT_$fCompareD6D7LT_$fCompareD6D6EQ_$fCompareD6D5GT_$fCompareD6D4GT_$fCompareD6D3GT_$fCompareD6D2GT_$fCompareD6D1GT_$fCompareD6D0GT_$fCompareD5:.LT_$fCompareD5D9LT_$fCompareD5D8LT_$fCompareD5D7LT_$fCompareD5D6LT_$fCompareD5D5EQ_$fCompareD5D4GT_$fCompareD5D3GT_$fCompareD5D2GT_$fCompareD5D1GT_$fCompareD5D0GT_$fCompareD4:.LT_$fCompareD4D9LT_$fCompareD4D8LT_$fCompareD4D7LT_$fCompareD4D6LT_$fCompareD4D5LT_$fCompareD4D4EQ_$fCompareD4D3GT_$fCompareD4D2GT_$fCompareD4D1GT_$fCompareD4D0GT_$fCompareD3:.LT_$fCompareD3D9LT_$fCompareD3D8LT_$fCompareD3D7LT_$fCompareD3D6LT_$fCompareD3D5LT_$fCompareD3D4LT_$fCompareD3D3EQ_$fCompareD3D2GT_$fCompareD3D1GT_$fCompareD3D0GT_$fCompareD2:.LT_$fCompareD2D9LT_$fCompareD2D8LT_$fCompareD2D7LT_$fCompareD2D6LT_$fCompareD2D5LT_$fCompareD2D4LT_$fCompareD2D3LT_$fCompareD2D2EQ_$fCompareD2D1GT_$fCompareD2D0GT_$fCompareD1:.LT_$fCompareD1D9LT_$fCompareD1D8LT_$fCompareD1D7LT_$fCompareD1D6LT_$fCompareD1D5LT_$fCompareD1D4LT_$fCompareD1D3LT_$fCompareD1D2LT_$fCompareD1D1EQ_$fCompareD1D0GT_$fCompareD0:.LT_$fCompareD0D9LT_$fCompareD0D8LT_$fCompareD0D7LT_$fCompareD0D6LT_$fCompareD0D5LT_$fCompareD0D4LT_$fCompareD0D3LT_$fCompareD0D2LT_$fCompareD0D1LT_$fCompareD0D0EQ_$fAddxyz $fAdd_:.yz $fAdd_:.yz0 $fAdd_:.yz1 $fAdd_:.yz2 $fAdd_:.yz3 $fAdd_:.yz4 $fAdd_:.yz5 $fAdd_:.yz6 $fAdd_:.yz7 $fAdd_:.y:. $fAdd_D9yy9 $fAdd_D8yy8 $fAdd_D7yy7 $fAdd_D6yy6 $fAdd_D5yy5 $fAdd_D4yy4 $fAdd_D3yy3 $fAdd_D2yy2 $fAdd_D1yy1 $fAdd_D0yy $fSnoc:.d':. $fSnocD9d:. $fSnocD8d:. $fSnocD7d:. $fSnocD6d:. $fSnocD5d:. $fSnocD4d:. $fSnocD3d:. $fSnocD2d:. $fSnocD1d:. $fSnocD0D9D9 $fSnocD0D8D8 $fSnocD0D7D7 $fSnocD0D6D6 $fSnocD0D5D5 $fSnocD0D4D4 $fSnocD0D3D3 $fSnocD0D2D2 $fSnocD0D1D1 $fSnocD0D0D0 $fSucc:.:. $fSucc:.:.0 $fSucc:.:.1 $fSucc:.:.2 $fSucc:.:.3 $fSucc:.:.4 $fSucc:.:.5 $fSucc:.:.6 $fSucc:.:.7 $fSucc:.:.8 $fSuccD9:. $fSuccD8D9 $fSuccD7D8 $fSuccD6D7 $fSuccD5D6 $fSuccD4D5 $fSuccD3D4 $fSuccD2D3 $fSuccD1D2 $fSuccD0D1$fReifies*:.Integer$fReifies*:.Integer0$fReifies*:.Integer1$fReifies*:.Integer2$fReifies*:.Integer3$fReifies*:.Integer4$fReifies*:.Integer5$fReifies*:.Integer6$fReifies*:.Integer7$fReifies*:.Integer8$fReifies*D9Integer$fReifies*D8Integer$fReifies*D7Integer$fReifies*D6Integer$fReifies*D5Integer$fReifies*D4Integer$fReifies*D3Integer$fReifies*D2Integer$fReifies*D1Integer$fReifies*D0Integer$fNat_:. $fNat_:.0 $fNat_:.1 $fNat_:.2 $fNat_:.3 $fNat_:.4 $fNat_:.5 $fNat_:.6 $fNat_:.7 $fNat_:.8$fNat_D9$fNat_D8$fNat_D7$fNat_D6$fNat_D5$fNat_D4$fNat_D3$fNat_D2$fNat_D1$fNat_D0 $fNatNE0_:. $fNatNE0_:.0 $fNatNE0_:.1 $fNatNE0_:.2 $fNatNE0_:.3 $fNatNE0_:.4 $fNatNE0_:.5 $fNatNE0_:.6 $fNatNE0_:.7 $fNatNE0_:.8 $fNatNE0_D9 $fNatNE0_D8 $fNatNE0_D7 $fNatNE0_D6 $fNatNE0_D5 $fNatNE0_D4 $fNatNE0_D3 $fNatNE0_D2 $fNatNE0_D1 $fDigit_D9 $fDigit_D8 $fDigit_D7 $fDigit_D6 $fDigit_D5 $fDigit_D4 $fDigit_D3 $fDigit_D2 $fDigit_D1 $fDigit_D0 $fNatNE0n$fNatnbaseGHC.IntInt8 fin2proxyGHC.ShowshowshowsGHC.EnumminBoundmaxBoundcheckingGHC.Baseconst _checking_OOR___thick_impossible_succ_maxBound_pred_minBound _toEnum_OOR $fSerialFin $fSerialFin0$fCoArbitraryFin$fArbitraryFin$fIxFin $fEnumFin$fDownwardEnumFin$fUpwardEnumFin $fEnumFin0 $fBoundedFin$fOrdFin$fEqFin $fReadFin $fShowFinInt16Int32Int64 integer-gmpGHC.Integer.TypeInteger