lyxia 2017-02-21 05:45:25
no
codedmart 2017-02-21 05:45:46
glguy: And then I just use that before forkIO ?
erisco 2017-02-21 05:45:48
Refl :: a :~: a and so say you are given some x :: a :~: b
codedmart 2017-02-21 05:45:59
Still trying to grasp.
erisco 2017-02-21 05:46:21
what happens in case x of Refl -> m ? well in m we have x :: a :~: b and x :: a :~: a (because x is Refl)
erisco 2017-02-21 05:46:34
so how does that unify? well, it must be that b = a
glguy 2017-02-21 05:46:45
codedmart: I'm not sure which part you're unsure about.
nitrix 2017-02-21 05:47:09
codedmart: Pasting what you have on lpaste.net might help from this point.
codedmart 2017-02-21 05:47:51
glguy: If I write a function from App a -> IO a. Just not sure how to use it. I guess I will write that function and try.
merijn 2017-02-21 05:48:10
ph88: witness just is a fancy way of saying 'a proof' (it is "a witness" to the fact that some predicate is true")
glguy 2017-02-21 05:48:27
codedmart: It'd be a normal function. You'd apply it as in applying f to x: 'f x'
codedmart 2017-02-21 05:49:02
I know that I meant in the context of forkIO, but let me just give it a go first. Then circle back.
codedmart 2017-02-21 05:49:03
Thanks
ph88 2017-02-21 05:55:05
lyxia, still don't know what you mean with pattern match in context of eqT :\
ph88 2017-02-21 05:57:31
https://hackage.haskell.org/package/base-4.9.1.0/docs/Data-Typeable.html#t::-126-:
ph88 2017-02-21 05:57:35
Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.
ph88 2017-02-21 05:57:49
no idea what this is talking about
codedmart 2017-02-21 05:57:53
glguy: So if I usually have `IO (Either ServantErr a)` when I unstack. To get to `IO a` what is the common thing to do with the Left branch? `error`?
glguy 2017-02-21 05:58:18
codedmart: That's up to you. There's no default answer. Why are you forking? What do you want to do if the think you forked failed?
ph88 2017-02-21 05:58:38
is there a search engine for haskell example code maybe ?
codedmart 2017-02-21 05:59:01
Just log it, but that should happen in LogM if I am thinking correctly. I am forking to run something in the background.
codedmart 2017-02-21 05:59:46
glguy: As long as I am thinking correct and LogM will log any error I would just like to ignore the Left.
lpaste_ 2017-02-21 06:01:10
lyxia pasted "ph88 how do you write this without pattern matching on r." at http://lpaste.net/352818
ph88 2017-02-21 06:02:17
oooh you pass the type variables down to the lower function
ph88 2017-02-21 06:02:23
so instead of b i could a concrete type there
ph88 2017-02-21 06:02:57
thanks lyxia !
ph88 2017-02-21 06:03:12
i was just used to pattern match on values
lyxia 2017-02-21 06:04:28
well Refl is a value
ph88 2017-02-21 06:04:49
yeah i just thought the pattenr matching was about the (a :~: b) part !!
ph88 2017-02-21 06:05:08
" pattern-match on the a :~: b "
ph88 2017-02-21 06:05:16
it says in the text
codedmart 2017-02-21 06:06:20
glguy: If I use `error` in the Left will that cause problems for the main thread of my app or just that thread? Not sure what else to use?
pikajude 2017-02-21 06:10:57
does anyone in here use docker for local development in conjunction with GHC
ph88 2017-02-21 06:12:52
i'm relieved to know that it's possible to compare types in haskell pfew
gracjan 2017-02-21 06:15:20
hi, a question
gracjan 2017-02-21 06:15:32
I do not understand spacing requirements for -XTypeApplication
gracjan 2017-02-21 06:15:46
why is `read@ Int "4"` problematic?
pikajude 2017-02-21 06:15:48
iirc it's @Type or @(Longer Type)
pikajude 2017-02-21 06:15:54
otherwise the parser gets confused
pikajude 2017-02-21 06:16:02
yeah you can't have a space there
gracjan 2017-02-21 06:16:07
why?
pikajude 2017-02-21 06:16:17
because that's the rule
pikajude 2017-02-21 06:16:23
i don't know
gracjan 2017-02-21 06:16:26
Prelude> let x @ Nothing = Just "abc" in print x
gracjan 2017-02-21 06:16:27
*** Exception: :4:5-28: Irrefutable pattern failed for pattern x@Nothing
gracjan 2017-02-21 06:16:37
I can have spaces in patterns
pikajude 2017-02-21 06:16:44
a type application isn't a pattern
pikajude 2017-02-21 06:16:56
they're entirely separate. the only similarity is the use of @
Tuplanolla 2017-02-21 06:17:14
What problem does disallowing spaces solve?
gracjan 2017-02-21 06:17:14
type application is always in expression context, isn't it?
gracjan 2017-02-21 06:18:14
What problem does requiring spaces solve/
gracjan 2017-02-21 06:18:15
?
gracjan 2017-02-21 06:18:49
it does not locally distinguish from patterns, as patters can have as many spaces as they want
gracjan 2017-02-21 06:19:06
so, what is the point?
glguy 2017-02-21 06:22:10
gracjan: https://github.com/ghc/ghc/blob/master/compiler/parser/Lexer.x#L533-L558
gracjan 2017-02-21 06:23:36
Example for this: "because we want to allow type patterns within expression patterns"?
Sonolin 2017-02-21 06:43:59
j
