erisco 2017-02-05 13:48:17
jle`, any hints with negation? I have seen a -> Void used but I can't see what this really informs the type checker of
erisco 2017-02-05 13:50:33
I can't construct an a -> Void either
xcmw 2017-02-05 14:01:42
How can I configure stack to use ghc 8.0.3? I need a bugfix that did not make 8.0.2
kadoban 2017-02-05 14:02:08
Do you need it to install it too?
Koterpillar 2017-02-05 14:02:15
xcmw: compiler-check: newer-minor?
kadoban 2017-02-05 14:02:31
Ya, mostly that ^
Koterpillar 2017-02-05 14:02:49
https://github.com/commercialhaskell/stack/blob/master/doc/yaml_configuration.md#compiler
kadoban 2017-02-05 14:02:55
Though you can specify exactly 8.0.2 if you like as well, not really sure which is the better idea in general.
Ptival 2017-02-05 14:03:28
so, the only way to flip two arguments of a type constructor is to make a newtype?
Ptival 2017-02-05 14:03:46
(if one wishes to eventually partially apply it)
erisco 2017-02-05 14:03:51
yes
Ptival 2017-02-05 14:03:56
thanks
tapirus 2017-02-05 14:05:13
Beginner question: what'd be the most idiomatic way to do something like somethingLikePrint [1,2,3,4] so that it prints '1 2 3 4' without quotes
erisco 2017-02-05 14:06:02
> (unwords . fmap show) [1,2,3,4]
lambdabot 2017-02-05 14:06:05
"1 2 3 4"
Koterpillar 2017-02-05 14:06:07
> traverse print [1, 2, 3, 4]
lambdabot 2017-02-05 14:06:10
Koterpillar 2017-02-05 14:06:13
err
erisco 2017-02-05 14:06:36
well then you'd use print, not show
erisco 2017-02-05 14:06:45
can't make lambdabot do that afaik
kadoban 2017-02-05 14:07:21
Was going to say something like: putStrLn . unwords . map show
erisco 2017-02-05 14:07:50
or I guess print is putStrLn . show
xcmw 2017-02-05 14:07:58
Koterpillar: That does not work for me. stack build does nothing after changing that. 8.0.3 is not released yet
Koterpillar 2017-02-05 14:08:33
xcmw: what about compiler: as I linked later?
jle` 2017-02-05 14:08:38
erisco: the (a -> Void) negation in haskell is mostly useful because it 'composes'
jle` 2017-02-05 14:08:54
you can build complex negation proofs by composing simpler ones that you might get
kadoban 2017-02-05 14:09:07
xcmw: stack is very unlikely to know how to install 8.0.3 for you, so you'll probably have to do that part yourself and use --system-ghc, or figure out how to teach it, which I forget how you do
hpc 2017-02-05 14:09:14
erisco: for certain a you are able to construct it
hpc 2017-02-05 14:09:35
erisco: you can't provide proof that anything implies false, but you can prove that false implies false
erisco 2017-02-05 14:09:40
okay I just need to see it in action then... what is the double negation proof i.e. ((a -> Void) -> Void) -> a ?
erisco 2017-02-05 14:09:49
it doesn't even seem to make sense =\
jle` 2017-02-05 14:09:58
erisco: and you can make some "primitive" (a -> Void)'s whenever you have a type 'a' with no constructors
jle` 2017-02-05 14:10:05
foo = \case {}
hpc 2017-02-05 14:10:07
double-negation elimination can't be written constructively
jle` 2017-02-05 14:10:17
erisco: double negation is not something you have in haskell
hpc 2017-02-05 14:10:26
you can do quad-to-double though
hpc 2017-02-05 14:10:32
and that's join for the "classical" monad
hpc 2017-02-05 14:10:50
join :: ¬¬(¬¬a) -> ¬¬a
jle` 2017-02-05 14:11:01
but you can prove like, say, if (n = m) is not true, then so is (S n = S m)
jle` 2017-02-05 14:11:16
erisco: that would go like ((n = m) -> Void) -> (S n = S m) -> Void
jle` 2017-02-05 14:11:26
s/so/neither
hpc 2017-02-05 14:11:34
@djinn ((((a -> Void) -> Void) -> Void) -> Void) -> ((a -> Void) -> Void) -> a
lambdabot 2017-02-05 14:11:34
-- f cannot be realized.
hpc 2017-02-05 14:11:38
@djinn ((((a -> Void) -> Void) -> Void) -> Void) -> ((a -> Void) -> Void)
lambdabot 2017-02-05 14:11:38
f a b = void (a (\ c -> void (c b)))
hpc 2017-02-05 14:12:03
cool, i didn't even know if djinn knew Void
erisco 2017-02-05 14:12:23
okay, so if we wanted a logic with double negation we'd have to choose something else for negation
erisco 2017-02-05 14:12:33
double negation elimination
hpc 2017-02-05 14:12:44
or we can embed it inside another double-negation
hpc 2017-02-05 14:13:15
and you can eliminate all but one of those doubles
erisco 2017-02-05 14:13:40
jle`, okay, so lets take your last example... what would that proof look like?
erisco 2017-02-05 14:13:44
again it doesn't make sense to me
hpc 2017-02-05 14:14:55
erisco: you would use (S n = S m) -> (n = m)
jle` 2017-02-05 14:15:05
foo f x = f (predEq x)
jle` 2017-02-05 14:15:18
where, yeah, predEq :: (S n = S m) -> (n = m)
hpc 2017-02-05 14:15:35
it turns refl :: (S n = S m) into refl :: (n = m)
jle` 2017-02-05 14:15:35
so in that case foo :: ((n = m) -> Void) -> (S n = S m) -> Void
hpc 2017-02-05 14:15:41
and then you pass it on to the function you got
hpc 2017-02-05 14:16:06
erisco: have you tried agda yet?
hpc 2017-02-05 14:16:59
if you haven't, you're pretty much ready for it with these sorts of questions and it opens a whole new area of type theory
halogenandtoast 2017-02-05 14:17:22
If I have `data NhkDateGrouping = NhkDateGrouping (Map String [NhkArticle])` and I want to get the array out, how can I do that, I'm trying `printDateGrouping (NhkDateGrouping (Map _ xs)) = undefined` but I'm getting `Not in scope: data constructor 'Map'` so I feel like I have something fundamentally wrong.
erisco 2017-02-05 14:17:30
I am getting along with Haskell for now. Still lots to figure out
jle` 2017-02-05 14:17:53
halogenandtoast: Map is a type
erisco 2017-02-05 14:17:54
I see how the proof works. I'll have to mull it over some
jle` 2017-02-05 14:18:03
it doesn't "contain" an array
hpc 2017-02-05 14:18:06
halogenandtoast: you can't pattern match on Map
jle` 2017-02-05 14:18:09
its data constructor isn't Map
xcmw 2017-02-05 14:18:10
kadoban: How would I do that? I need https://git.haskell.org/ghc.git/commitdiff/3540d1e1a23926ce0a8a6ae83a36f5f6b2497ccf or later
jle` 2017-02-05 14:18:28
halogenandtoast: 'Map _ xs' isn't the constructor of a type (Map String [NhkArticle])
hpc 2017-02-05 14:18:32
halogenandtoast: (Map String [foo]) is a key-value data structure that looks up values of type [foo] by values of type String
jle` 2017-02-05 14:18:35
halogenandtoast: are you familiar with constructors, and types?
jle` 2017-02-05 14:18:48
like, for example, 'Maybe Int' has two constructors, 'Just x' and 'Nothing'
hpc 2017-02-05 14:18:51
halogenandtoast: so you would instead do printDateGrouping (NhkDateGrouping map) = ...
halogenandtoast 2017-02-05 14:19:00
jle`: briefly, and I'm not sure why I thought that was possible...
jle` 2017-02-05 14:19:02
and if you have a value of type 'Maybe Int', you could pattern match on the 'Just x' and 'Nothing' constructors
hpc 2017-02-05 14:19:08
halogenandtoast: and inside "..." you would look up in the map by some particular string
halogenandtoast 2017-02-05 14:19:08
Right
hpc 2017-02-05 14:19:19
halogenandtoast: and decide what to do if you don't find anything
jle` 2017-02-05 14:19:27
but, 'Map String [NhkArticle]''s constructor is *not* 'Map s xs'
hpc 2017-02-05 14:19:28
(since not all keys map to values)
jle` 2017-02-05 14:19:44
in general, for most types, the constructor isn't the same as the type name
jle` 2017-02-05 14:20:07
(see Maybe and Just/Nothing)
hpc 2017-02-05 14:20:16
halogenandtoast: as for keeping straight what level (type or value) you are at, consider the following:
hpc 2017-02-05 14:20:26
halogenandtoast: data Bool = False | True
hpc 2017-02-05 14:20:32
foo :: Bool -> String
hpc 2017-02-05 14:20:34
foo False = ""
hpc 2017-02-05 14:20:37
foo True = "yes"
jle` 2017-02-05 14:20:52
halogenandtoast: if you're using Map from the standard libraries, 'Map' is implemented as an abstract data type, so it actually doesn't expose any constructors directly
halogenandtoast 2017-02-05 14:21:05
Yeah as soon as you guys said that, I realized how absurd I was being.
kadoban 2017-02-05 14:21:05
xcmw: Which part? Telling stack how to install a different GHC version? I'd have to look it up.
jle` 2017-02-05 14:21:07
halogenandtoast: you have to manipulate it using the API that the Data.Map module exports for the type
halogenandtoast 2017-02-05 14:21:20
I blame it being early
jle` 2017-02-05 14:21:29
that's fair :)
halogenandtoast 2017-02-05 14:21:41
*blame it on being early
hpc 2017-02-05 14:21:41
halogenandtoast: it's really hard to keep straight when you're still new to the syntax :)
hpc 2017-02-05 14:22:15
it'll get really easy with just more exposure to it
Ptival 2017-02-05 14:24:27
erisco: do you know if there's a standard way of naming the function extract :: FlippedSomething a b -> Something b a?
Koterpillar 2017-02-05 14:25:00
unFlipped?
erisco 2017-02-05 14:25:01
usually if your newtype's name is X the field is called runX or unX or getX
Ptival 2017-02-05 14:25:17
ah, unX sounds good yeah
xcmw 2017-02-05 14:29:07
kadoban: The entire thing. A link to instructions is fine. My googling is not coming up with anything
halogenandtoast 2017-02-05 14:29:38
Next, probably dumb, question... If I have `data NhkDateGrouping = NhkDateGrouping (Map String [NhkArticle]) ` and `printDateGrouping (NhkDateGrouping m) = (printNhkArticles . elems) m` and finally `printNhkArticles :: [NhkArticle] -> IO ()` why am I getting `Couldn't match type 'NhkArticle' with '[NhkArticle]'`
halogenandtoast 2017-02-05 14:29:55
nvm I think I know
halogenandtoast 2017-02-05 14:30:00
I need to flatten
halogenandtoast 2017-02-05 14:30:03
`concat`
halogenandtoast 2017-02-05 14:30:47
and that was correct.
Ptival 2017-02-05 14:36:16
q: if I have data Foo (φ :: * -> *) ξ = MkFoo (φ ξ) is there anything I can pass to Foo to get the effect of identity?
Koterpillar 2017-02-05 14:37:42
Data.Functor.Identity.Identity
jle` 2017-02-05 14:41:38
Foo is IdentityT
jle` 2017-02-05 14:41:50
so you could pass in Identity, heh
jle` 2017-02-05 14:42:07
IdentityT Identity = Identity
jle` 2017-02-05 14:42:21
er, s/=/is isomorphic to
jle` 2017-02-05 14:42:35
well IdentityT f ~ f, in general
xcmw 2017-02-05 14:43:25
kadoban: I found instructions. I think I see how to do it
