Haskell Channel Logs: #haskell channel featuring zipper, johndcl, srhb, mniip, sL1Me, MP2E, and 8 others.

johndcl 2017-02-03 21:49:27

glguy: http://lpaste.net/2420610067280691200 not even now?

glguy 2017-02-03 21:49:58

opqdonut 2017-02-03 21:50:02

haskell tries equations in order, and matches the arguments in order

johndcl 2017-02-03 21:50:29

ok, that is awesome, thank you

opqdonut 2017-02-03 21:50:31

so it starts with comparing the first argument with (Just m). the first argument is reduced until it produces a Maybe consructor

opqdonut 2017-02-03 21:50:56

if the first argument turns out to be Nothing, the first equation can't match, so haskell moves on to the second equation

opqdonut 2017-02-03 21:51:07

which matches everything

opqdonut 2017-02-03 21:51:11

so Nothing is returned

zipper 2017-02-03 21:51:35

Hey what can get me from ["we" "are"] to "we are" ?

johndcl 2017-02-03 21:51:43

thank you

srhb 2017-02-03 21:52:18

zipper: Did you mean ["we","are"]

opqdonut 2017-02-03 21:52:20

> intercalate " " ["we", "are"] -- zipper

lambdabot 2017-02-03 21:52:22

"we are"

glguy 2017-02-03 21:52:33

unwords

opqdonut 2017-02-03 21:52:49

oh, unwords, yeah

zipper 2017-02-03 21:56:40

Thanks for unwords

knupfer 2017-02-03 21:56:50

> const "we are" "[\"we\" \"are\"]"

lambdabot 2017-02-03 21:56:52

"we are"

knupfer 2017-02-03 21:56:53

MP2E 2017-02-03 21:57:03

hah :p

knupfer 2017-02-03 21:58:45

What's currently going on in GHC-HQ, can we espect fancy new optimizations or language features?

Axman6 2017-02-03 22:03:05

riaqn: riaqn: it's not widely used (yet?), but this is under development where I work: https://gitlab.anu.edu.au/mu/mu-spec/blob/master/overview.rst

Axman6 2017-02-03 22:03:15

uh, only one riaqn :)

mniip 2017-02-03 22:11:00

is end the forall or the exists?

ski 2017-02-03 22:11:59

`forall'

ski 2017-02-03 22:18:38

given `F : C^Op * C >---> D', the end of `F' is specified by : `End F', which is `forall c : C. F(c,c)' (aka ⌜∫_c F(c,c)⌝ or ⌜∫_C D⌝), is an object of `D'; `omega : forall c : C. (End F >---> F(c,c))', iow `omega_c : (forall c : C. F(c,c)) >---> F(c,c)' (for all `c' in `C') is a dinatural transformation

sL1Me 2017-02-03 22:19:19

Any Really Good AHK Coder here who can help me?

mniip 2017-02-03 22:20:39

you're probably talking about auto haskell key

mniip 2017-02-03 22:20:46

which makes a lot of sense in a haskell channel

ski 2017-02-03 22:22:10

such that for any object `e' of `D' with dinatural `beta : forall c : C. (e >---> F(c,c))', there exists a unique morphism `poly_beta : e >---> (forall c : C. F(c,c))' in `D' satisfying `omega_c . poly_beta = beta_c'

mniip 2017-02-03 22:23:49

hmmmm

mniip 2017-02-03 22:24:00

I was expecting it to be simpler

ski 2017-02-03 22:24:07

in the case of categorical products, the "there exists a unique morphism ... satisfying [commuting diagram]" says that (given `f : T >---> A' and `g : T >---> B') there exists a morphism ` : T >---> A * B', satisfying (in terms of points) `(t) = (f t,g t)' (in haskell `' is called `f &&& h', at least when using the `Arrow' terminology)

ski 2017-02-03 22:25:29

in this case, it tells you that if you have something (`beta') of type `forall c. ... -> F c c' (where `F' is contravariant in one argument, and covariant in the other), `...' not depending on `c', then you can think of it as something (`poly_beta') of type `... -> (forall c. F c c)'

ski 2017-02-03 22:26:24

so it's merely moving the `forall', going from `forall c. ... -> ..c..' to `... -> (forall c. ..c..)', but with `..c..' here depending both contravariantly and covariantly on `c'

mniip 2017-02-03 22:26:25

denotes the mediating morphism for the product?

ski 2017-02-03 22:26:28

yes

mniip 2017-02-03 22:26:32

or is there a more elaborate definition

ski 2017-02-03 22:27:00

in the case of *co*ends, it's instead about going from `forall c. ..c.. -> ...' to `(exists c. ..c..) -> ...'

ski 2017-02-03 22:27:51

so it's telling you that you can inspect an existential input, if you're prepared to be, in your use of the innards, polymorphic in the existentially quantified variable

ski 2017-02-03 22:28:38

(still similarly talking about the case of difunctors, so `c' may occur both contravariantly and covariantly in `..c..')

mniip 2017-02-03 22:29:36

I'm trying to grasp the generic definitions

mniip 2017-02-03 22:29:43

I know what forall/exists do in Hask

ski 2017-02-03 22:29:45

mniip : in categorical semantics, you interpret an *expression* `e' as a morphism described by the mapping from the (values of) the set of free variables `FV(e)' to the corresponding value of `e'

mniip 2017-02-03 22:29:47

probably too well

ski 2017-02-03 22:30:26

so `x + y^2', construed as depending on variables `x',`y',`z' (the last vacuously) will be interpreted as a morphism `(x,y,z) |-> x + y^2'

ski 2017-02-03 22:31:35

`Gamma |- e : tau' gets translated to `|e|_{Gamma,tau} : |Gamma| >---> |tau|', where in this case `|x : Integer,y : Integer,z : Integer| becomes `Integer * Integer * Integer'

ski 2017-02-03 22:33:26

in this situation, the *expression* `(e0,e1)', becomes `', assuming `e0' becomes `f' and `e1' becomes `g'

ski 2017-02-03 22:36:14

so i suppose what i'm trying to say here is that the "exists unique" in situations like this typically means that you get some construction in the (internal) language for constructing or deconstructing (depending on whether the new object, characterized by the universal mapping principle, in the category is on the codomain or the domain end of the arrow) "values in the object"

ski 2017-02-03 22:37:14

in the case of `', this is how you make a morphism *into* a categorical product, by constructing it from one morphism into each factor, all morphisms having the same domain (`|Gamma|')