erisco 2017-02-06 14:45:15
this is what I meant yesterday by my inability to construct an a -> Void
erisco 2017-02-06 14:45:40
given some A -> Void I can, like your example demonstrated, but otherwise I'm stuck
erisco 2017-02-06 14:46:27
I can construct the relation of unequal naturals...
erisco 2017-02-06 14:47:56
it seems like a -> Void is good for a :: * but not for other kinds
erisco 2017-02-06 14:48:14
so perhaps I need to classify the notation of negation
jle` 2017-02-06 14:48:19
er, a := b :: *, there
erisco 2017-02-06 14:48:21
the notion*
erisco 2017-02-06 14:48:28
yes that is correct
jle` 2017-02-06 14:48:44
(a :< b) -> Not (a := b) makes sense as a thing
jle` 2017-02-06 14:49:04
but giving it comes from the nature of the structure of your (a :< b) proof
jle` 2017-02-06 14:49:32
what witness you have for (a :< b)
erisco 2017-02-06 14:49:47
LtZ and LtS
jle` 2017-02-06 14:51:06
say, data (:<) :: N -> N -> * where LtZ :: n :< S m; LtS :: n :< m -> S n :< S m ... ?
jle` 2017-02-06 14:51:27
* LtZ :: Z :< S m
erisco 2017-02-06 14:52:28
well I chose LtZ :: Sing m -> Z :< S m but I suppose either works
erisco 2017-02-06 14:53:03
could use that or SingI m context
erisco 2017-02-06 14:55:36
in the example that had form (A -> Void) -> (B -> Void) I understood because we can map A to B with B -> A
jle` 2017-02-06 14:55:50
in that case your first branch could be foo = \case LtZ s -> case s of SS s -> \case {}
erisco 2017-02-06 14:55:57
we're not concerned whether an A -> Void actually exists, it is given to us
erisco 2017-02-06 14:56:15
but in this scenario we have to just give an a := b -> Void
jle` 2017-02-06 14:56:17
er wait hm, let me think through the syntax of the second half
erisco 2017-02-06 14:56:18
how is that ever possible
jle` 2017-02-06 14:56:33
you can give an (a := Void) with empty patterns
jle` 2017-02-06 14:56:41
er, empty case statements
jle` 2017-02-06 14:57:15
foo = \case LtZ s -> case s of S _ -> \case {}
erisco 2017-02-06 14:57:27
but what inhabitant of a := b -> Void is that? aren't we just writing undefined?
jle` 2017-02-06 14:57:43
`\case {}` handles every possible input case
jle` 2017-02-06 14:57:49
because there are no possible inputs
jle` 2017-02-06 14:58:06
voidId :: Void -> Int; voidId = \case {}, for example
erisco 2017-02-06 14:58:09
ah ha, got ya
jle` 2017-02-06 14:58:17
so \case {}, or \x -> case x of {}
jle` 2017-02-06 14:58:37
um, in explicit mode, it'd be case s of S _ -> \noSuchRefl -> case noSuchRefl of {}
erisco 2017-02-06 14:58:38
this is an aspect of A -> Void I did not consider!
erisco 2017-02-06 14:58:41
what if there are no A's!
jle` 2017-02-06 14:58:45
because there isn't any possible consturctor
jle` 2017-02-06 14:58:52
so you don't have to handle any cases
jle` 2017-02-06 14:58:54
mhm
erisco 2017-02-06 14:58:58
right right, okay thanks
erisco 2017-02-06 14:59:07
can't believe I didn't see that. thanks!
jle` 2017-02-06 14:59:09
unfortunately right now GHC doesn't warn you if you do \case {} and there actually 'are' constructors
jle` 2017-02-06 14:59:13
no problem, it's not obvious!
jle` 2017-02-06 14:59:25
ideally \case {} should give incomplete pattern match warning
erisco 2017-02-06 14:59:27
it doesn't? darn... so it sounds more like undefined then
jle` 2017-02-06 14:59:44
well, it's actually the other problem
jle` 2017-02-06 14:59:58
if you try to put in any pattern, GHC will complain. so that's good
jle` 2017-02-06 15:00:12
like, if you accidentally did \case Refl -> ..., GHC will complain that Refl isn't a possible constructor
jle` 2017-02-06 15:00:18
so it's better than undefined in that sense
erisco 2017-02-06 15:00:39
so it knows which constructors are excluded but not that they are all excluded
Ptival 2017-02-06 15:00:46
would you write "return Nothing <$> p" or "p *> Nothing" or something else?
erisco 2017-02-06 15:00:47
sounds like that could be improved in a patch later on
jle` 2017-02-06 15:01:10
yeah i don't think this is any fundamental property of the type system/ghc...probably just some switch in ghc turned off
Ptival 2017-02-06 15:01:31
sorry, would you write "return Nothing <$> p" or "p *> return Nothing" or something else where "return" does not need to appear?
jle` 2017-02-06 15:01:33
Ptival: 'Nothing <$ p', maybe?
jle` 2017-02-06 15:01:52
it's also kind of silly to use return there....what you write is basically 'const Nothing <$> p'
jle` 2017-02-06 15:01:57
because 'return' is the (->) instance
jle` 2017-02-06 15:02:09
you meant (\_ -> Nothing) <$> p, right?
jle` 2017-02-06 15:02:15
in that case, you can do Nothing <$ p
jle` 2017-02-06 15:02:56
return Nothing <$> p is the same as p *> return Nothing, but the return's are different :) kind of a coincidence there
Welkin 2017-02-06 15:05:41
const Nothing <$> p
Welkin 2017-02-06 15:05:46
so many ways to write it!
erisco 2017-02-06 15:06:28
EmptyCase on but (\case {}) is a parse error on case... hrm
erisco 2017-02-06 15:06:59
oh that is LambdaCase isn't it
jle` 2017-02-06 15:07:11
yeah
Welkin 2017-02-06 15:07:12
lol
erisco 2017-02-06 15:15:49
does ¬Q ⇒ ¬P have a name? I thought it did
jle` 2017-02-06 15:18:13
just sounds like a normal implication
jle` 2017-02-06 15:18:22
is there some relationship between P and Q that you aren't mentioning
jle` 2017-02-06 15:18:30
if P => Q, then what you said is the contrapositive
alexashka 2017-02-06 15:26:14
good day - I'm wanting to run my haskell code on an ubuntu server, and I do my development on a mac. So I transferred the binary over, of course it won't run. Googling says it's the incompatible architectures. What gives? How do I compile my haskell goodies to run on ubuntu?
alexashka 2017-02-06 15:26:50
I imagine this isn't an exotic question, yet googling around isn't being very fruitful :(
ertes 2017-02-06 15:27:17
alexashka: the simple option is to compile on ubuntu
ertes 2017-02-06 15:27:36
alexashka: if you really want to compile on mac, you need to set up GHC as a cross-compiler
alexashka 2017-02-06 15:27:57
ertes: I decided to try that - running stack build halts on populating index cache
alexashka 2017-02-06 15:28:40
by halts I mean the process gets killed, I get 'Populating index cache ...Killed' - google says stack build takes up a lot of memory, and my digitalocean droplet only has so much
suzu 2017-02-06 15:29:18
alexashka do you have some free disk space?
suzu 2017-02-06 15:29:29
you can use some disk space as swap and dodge the ram requirement that way
alexashka 2017-02-06 15:29:29
suzu: yessir
alexashka 2017-02-06 15:29:45
that's a good idea - how's that done?
suzu 2017-02-06 15:29:59
so first make a big file
suzu 2017-02-06 15:30:16
sudo dd if=/dev/zero of=swapfile bs=1K count=4M
ertes 2017-02-06 15:30:19
another option is to use nix… building for darwin works here without any setup, as far as i can tell
suzu 2017-02-06 15:30:22
that'll make you a 4 gigabyte file of zeroes
ertes 2017-02-06 15:30:23
of course i can't test the result
ertes 2017-02-06 15:30:29
because i don't have a mac
suzu 2017-02-06 15:30:31
called 'swapfile'
suzu 2017-02-06 15:30:40
then you can turn it on
suzu 2017-02-06 15:30:45
mkswap swapfile
suzu 2017-02-06 15:30:48
swapon swapfile
suzu 2017-02-06 15:30:52
those two commands ^
suzu 2017-02-06 15:30:54
then try building
suzu 2017-02-06 15:31:09
when you're done, do `swapoff swapfile` and then destroy swapfile if you wish
alexashka 2017-02-06 15:31:21
suzu: very intereting, let me give that a try
alexashka 2017-02-06 15:31:49
ertes: you mean run a virutal machine, compile on there, and transfer that file over? so that the architectures match?
ertes 2017-02-06 15:32:10
alexashka: that would be the "just compile on ubuntu" option
ertes 2017-02-06 15:32:35
the second option is to cross-compile… it's painful to set up, but once done it's convenient
ertes 2017-02-06 15:32:40
the third option is to try nix
alexashka 2017-02-06 15:32:50
ertes: ya, I am leaning towards that - doing this swapon/off every time I need to build seems really o-O
alexashka 2017-02-06 15:32:57
I'm not sure what nix is, can you elaborate?
suzu 2017-02-06 15:33:09
you could just leave the swap on all the time
suzu 2017-02-06 15:33:39
it basically adds more memory to your system at the expense of speed.
ertes 2017-02-06 15:33:43
nix is a package/deployment manager which has cross-compilation built in by concept
alexashka 2017-02-06 15:34:28
hehe nix - Poor OS X support for stable releases
ertes 2017-02-06 15:34:46
well, use the unstable one =)
LeCamarade 2017-02-06 15:35:24
1
alexashka 2017-02-06 15:35:42
I'm going to give this swapping idea a try - I appreciate your ideas as well, thank you
ertes 2017-02-06 15:36:15
adding swap might turn an impossible task into an unbearably painful one… consider RAM compression first, if your OS supports it
