dram_phone 2017-02-01 20:45:25
It's getting difficult to explain, my mind's not clear
ski 2017-02-01 20:45:36
mniip : a pair term `(M,N)' gets translated to tupling of morphisms ` : Gamma >---> A * B', where `f : Gamma >---> A' and `g : Gamma >---> B' are the translations of the terms `M',`N', `Gamma' being their common context, converted to a product type as above
dram_phone 2017-02-01 20:46:33
ski: *Catching* (propagated) errors should be done sparingly
dram_phone 2017-02-01 20:46:51
Handling of alternatives occur everywhere
ski 2017-02-01 20:47:20
mniip : perhaps more clearly expressed, if `Gamma |- M : A' and `Gamma |- N : B', so that `Gamma |- (M,N) : A * B', `(M,N)' gets translated to ` : |Gamma| >---> A * B', assuming `M' translates to `f : |Gamma| >---> A' and `N' translates to `g : |Gamma| >---> B', `|Gamma|' being the translation of the typing context to a product type
ski 2017-02-01 20:48:01
dram_phone : i'm not sure i agree with "If you're using exceptions like 'if's you're doing it wrong" (depending on what you mean exactly by it)
mniip 2017-02-01 20:48:26
right
mniip 2017-02-01 20:48:36
but then there are exponentials
ski 2017-02-01 20:48:39
yep
dram_phone 2017-02-01 20:49:04
Screw it
dram_phone 2017-02-01 20:49:08
use whatever you want
ski 2017-02-01 20:49:22
mniip : so, in the internal language, we have that if `f : A >---> B' and `Gamma |- M : A', then `Gamma |- f M : B', application of a morphism to a term/expression
ski 2017-02-01 20:50:14
mniip : if `M' translates to `g : |Gamma| >---> A', then `f M' translates to `f . g : |Gamma| >---> B', so application of morphism just becomes composition
dram_phone 2017-02-01 20:51:02
I'm leaving this, my brain is like completely messed up
ski 2017-02-01 20:51:04
mniip : the more interesting case is `Gamma |- M $ N : B', in case `Gamma |- M : A -> B' and `Gamma |- N : A'
ski 2017-02-01 20:51:21
dram_phone : i was looking for a few links you might find interesting, but ...
ski 2017-02-01 20:53:32
mniip : one can either treat this case on its own .. or one can treat `M $ N' as a macro for `apply (M,N)', with `apply : (A -> B) * A >---> B'. in either case `M $ N' becomes `apply . : |Gamma| >---> B' assuming `M' becomes `f : |Gamma| >---> (A -> B)' and `N' becomes `g : |Gamma| >---> A'
ski 2017-02-01 20:55:27
mniip : then, we come to `Gamma |- \x |-> M : A -> B' holding when `Gamma , x : A |- M : B' .. here `M' must be translated in the extended context, with `x : A' added to it
ski 2017-02-01 20:56:34
mniip : the translation of `M' in that context will be some `f : |Gamma| * A >---> B', then the translation of `\x |-> M' in the context `Gamma' is simply `curry f : |Gamma| >---> (A -> B)'
samvher 2017-02-01 20:56:52
does anyone here have experience with the digestive-functors library? so far I managed to use it with no problems, but now I'm trying to use the "listOf" function and I can't quite figure it out
ski 2017-02-01 20:57:14
(`curry' is a contruction making a new morphism from an old one, just like tupling, `' makes a new morphism out of two old ones `f0',`f1')
ski 2017-02-01 20:59:26
mniip : if we want to be more explicit (but omitting the types), we can say that we translate `f,x |-> g (\y |-> f (x,y))' (a term-in-context) (the context in this case only explicitly mentioning the (possibly free) variables) by translating two two subterms-in-context `f,x |-> g' and `f,x |-> \y |-> f (x,y)'
ski 2017-02-01 21:00:50
mniip : the latter of is translated by translating the subterm-in-context `(f,x),y |-> f (x,y)', which requires translating the subterm-in-context `(f,x),y |-> (x,y)', which finally requires translating `(f,x),y |-> x' and `(f,x),y |-> y'
ski 2017-02-01 21:02:15
mniip : a variant is to not use binary products for the translation of the context itself, but instead use "indexed products" (record types). then the translation of each variable will be just a single projection, not a sequence of projections
ski 2017-02-01 21:03:46
mniip : in a topos, we also have a "subobject classifier" object, aka a "truth-value object", which we can think of roughly as `Bool' (though it need not be boolean/two-valued) or `Prop' (the type or kind of propositions)
ski 2017-02-01 21:06:03
mniip : if we write this object as `Omega' (traditional) we have `and,or,implies : Omega * Omega >---> Omega',`not : Omega >---> Omega' (`not' needn't be its own inverse, in general). for an object `X', we have quantifiers `forall_X,exists_X : (X -> Omega) >---> Omega'
ski 2017-02-01 21:06:54
mniip : a morphism from `A' to `Omega' is a property/predicate on `A'. a morphism from `A * B * ... * Z' to `Omega' is a relation between `A',`B',...,`Z'
ski 2017-02-01 21:08:19
mniip : an inhabitant of `A -> Omega' describes a "subset" of `A'. the elementhood relation `in : (A -> Omega) * A >---> Omega' is simply `apply'
ski 2017-02-01 21:09:26
mniip : `{x : A | ..x..}' a term of type `A -> Omega', iow a subset of A', is simply syntactic sugar for `\x |-> ..x..'
ski 2017-02-01 21:10:38
mniip : using this, one can express (intuitionistic !) logic, and set theory, inside any topos
ski 2017-02-01 21:16:14
mniip : e.g., in the category of (directed, loop-allowing, multi-)graphs, `Omega' is a graph with two nodes, say `True' and `False', and five edges, `true : True >---> True',`false : False >---> False',`ends : True >---> True' are loops on the nodes, and then there's also `source : True >---> False',`target : False >---> True' edges between the two nodes
ski 2017-02-01 21:18:18
mniip : this is used to describe the "truth-value" of a node or an edge being included in a subgraph of a graph `G'. the predicate `in_my_subgraph : G >---> Omega' will map nodes in `G' to `True' when they're in the subgraph, and to `False' when they're not
ski 2017-02-01 21:19:47
mniip : it'll map edges that are in the subgraph to `true', while if an edge is not in, but both its source and target ends are, it'll be mapped to `ends'. if only the source of it is in, then it's mapped to `source'. if only the target, then `target'
ski 2017-02-01 21:21:37
mniip : another example is the category of (discrete) dynamical systems. an object is a pair of a set `A' and an endofunction `f : A >---> A' (thought of as "taking a step of time"), morphisms are functions between sets, such that stepping time in the domain, and then converting to the codomain is the same as first converting to the codomain, and then stepping time
ski 2017-02-01 21:23:25
mniip : here, the subobject classifier `Omega' looks like `0 |---> 1 |---> 2 |---> ... infinity |-> infinity', `0' is "true", `infinity' is "false"
ski 2017-02-01 21:24:27
mniip : a predicate of type `D >---> Omega' describes a sub-(dynamical system) of `D', mapping points in `D' that are in to `0'/true; points that are outside, but will come inside in one step, to `1'; points that will come inside in two steps to `2'; ...; points that will never arrive inside to `infinity'
ski 2017-02-01 21:26:04
(once inside, you can never leave. this follows from the predicate being a morphism of dynamical systems, from `D' to `Omega'. it is also possible to describe another object `chaotic_Omega', so that morphisms to it correspond to arbitrary subsets, not just sub-(dynamical systems))
ski 2017-02-01 21:26:43
mniip : if you feel like, you could try figuring out how the categorical product, and the exponential object, looks like in these two categories
ski 2017-02-01 21:28:23
(also note that in both cases, `not' is not an involution (aka self-inverse), in the first case `not . not' maps `ends' to `true'. in the second case any positive (finite) integer is mapped to `0' (btw, what is `and' and `or' here ?))
nhooyr 2017-02-01 21:32:09
how does haskell compare to elixir for the web? in terms of concurrency and whatnot.
cocreature 2017-02-01 21:34:42
is the way ghc _implements_ exceptions described somewhere? I'm somewhat familiar with the way this is done in C++ compilers, but I'd imagine GHC does things differently
tsahyt 2017-02-01 21:38:41
I have a foldr that I'd like to make strict for testing purposes (profiling shows that a lot of allocations and time are spent there). is there any reason to use foldl' here instead of simply going with foldr'?
cocreature 2017-02-01 21:39:44
tsahyt: making foldr strict usually has no effect. e.g. if you use foldr (+) 0 to calculate the sum, you'd still end up with x + (y + (…)) and while you are walking through the list no evaluation can take place
tsahyt 2017-02-01 21:39:59
right, foldl' it is then
tsahyt 2017-02-01 21:40:11
I'm doing a bunch of inserts into a HashPSQ
cocreature 2017-02-01 21:40:15
tsahyt: for foldl on the other hand you end up with ((x + y) + z) + … so strictness forces GHC to do the sums immediately
tsahyt 2017-02-01 21:40:33
what is foldr' good for then?
cocreature 2017-02-01 21:41:01
I've never seen a good use for it :) (but ofc that doesn't mean that one doesn't exist)
ski 2017-02-01 21:41:15
tsahyt : `foldr' should typically be used when your list could be infinite ior you're computing a larger (incremental) structure as result, not just a small summary of the elements
cocreature 2017-02-01 21:42:00
ski: but when do you use foldr' over foldr?
ski 2017-02-01 21:42:12
i have never used foldr'
cocreature 2017-02-01 21:42:20
yeah me neither
cocreature 2017-02-01 21:42:37
I was surprised that this is even in "base" but apparently it is
opqdonut 2017-02-01 21:42:37
is there a foldr'?
tsahyt 2017-02-01 21:42:42
opqdonut: yes in Data.Foldable
cocreature 2017-02-01 21:42:43
it's in Data.foldable
opqdonut 2017-02-01 21:42:49
let's see
ski 2017-02-01 21:42:57
perhaps someone thought it should be added "for symmetry"
cocreature 2017-02-01 21:43:05
foldr' is implemented in terms of foldl …
opqdonut 2017-02-01 21:43:27
oh right it's in the Foldable class
opqdonut 2017-02-01 21:43:37
so a two-ended collection can implement an efficient fold
opqdonut 2017-02-01 21:43:55
that makes sense
opqdonut 2017-02-01 21:44:02
doesn't make any sense for lists though
ski 2017-02-01 21:44:04
i see
cocreature 2017-02-01 21:44:21
ah yeah for nonlists it makes sense
