dgpratt 2017-02-03 14:45:23
does anyone know, is it possible to tell ghci to ignore the standard .ghci file and possibly load a different one instead?
erisco 2017-02-03 14:45:24
right, hrm, makes sense. I guess they don't have a special case for these contexts
monochrom 2017-02-03 14:45:43
The GHC Users Guide says that banning existential newtype is just because the GHC people are too lazy to implement it and too few users asked. You can ask them if you want it happen.
jle` 2017-02-03 14:45:48
in this case you don't actually have a typeclass constraint, so i feel like it should technically be ok
erisco 2017-02-03 14:46:36
I'd only ask if I had a donation to throw at them
jle` 2017-02-03 14:46:46
erisco: you could recover newtypeness by skolemizing your existential, potentially
dgpratt 2017-02-03 14:47:12
that just sounds like word salad
jle` 2017-02-03 14:47:58
newtype BoundedAbove n = BoundedAbove (forall r. (forall m. (m :<= n) ~ True => SNat m -> r) -> r)
erisco 2017-02-03 14:47:59
I'd have to review skolems
Welkin 2017-02-03 14:48:01
lol
Welkin 2017-02-03 14:48:07
I remember skolems
Welkin 2017-02-03 14:48:12
no idea what they are though
jle` 2017-02-03 14:48:24
in that case you get a newtype, but .... you aren't storing an actual SNat m anymore
jle` 2017-02-03 14:48:40
so maybe it's not an actual gain heh
erisco 2017-02-03 14:48:58
well I'd say not, seeing as that is the point of it :P
Welkin 2017-02-03 14:49:08
"rigid type variable"
monochrom 2017-02-03 14:49:14
You can think of that as continuation-passing style and/or church encoding (more accurately Boehm-Bararducci encoding)
jle` 2017-02-03 14:49:18
dgpratt: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/ghci.html#the-ghci-files
erisco 2017-02-03 14:49:21
I see the idea but that is saying I can give any m later on
erisco 2017-02-03 14:49:27
rather than giving one now
jle` 2017-02-03 14:49:48
that's actually the opposite of the idea
dgpratt 2017-02-03 14:49:50
ah, excellent, thanks jle`
jle` 2017-02-03 14:50:10
the idea is that one m exists, and whatever it is, you're going to have to handle it in a uniform way
Welkin 2017-02-03 14:50:49
wow, this paper is 88 pages
Welkin 2017-02-03 14:50:50
http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/putting.pdf
Welkin 2017-02-03 14:50:56
but it reads pretty easily
erisco 2017-02-03 14:51:08
oh derp I missed it was (SNat m -> r) -> r not SNat m -> r
jle` 2017-02-03 14:51:42
um i have a brief skolemization tutorial in https://blog.jle.im/entry/practical-dependent-types-in-haskell-2.html
erisco 2017-02-03 14:51:54
I don't know how this relates to skolems but in effect we're just storing m in a closure
jle` 2017-02-03 14:51:54
if you wanted to hear what i'd say if you asked me for more detail
monochrom 2017-02-03 14:52:10
Be careful. (forall m. (constraints) => SNat m -> r) -> r
erisco 2017-02-03 14:52:14
so I don't think that is actually addressing the "moar speed pl0x" need
jle` 2017-02-03 14:52:31
well
jle` 2017-02-03 14:52:34
who knows :)
jle` 2017-02-03 14:52:41
(answer: the person that benchmarks)
monochrom 2017-02-03 14:53:09
You should benchmark and you may be surprised.
jle` 2017-02-03 14:53:28
i'm actually not sure which result would surprise me more
monochrom 2017-02-03 14:53:51
Because the way Oleg and edwardk and attoparsec gain their speed is by doing this.
erisco 2017-02-03 14:54:10
jle`, thanks for the article
Welkin 2017-02-03 14:54:14
lol
Welkin 2017-02-03 14:54:18
that is a funny grouping
jle` 2017-02-03 14:54:20
no problem!
erisco 2017-02-03 14:54:30
seems bizarre as to how it could help
Welkin 2017-02-03 14:54:39
so you are saying that Oleg and edwardk are just programs!?
monochrom 2017-02-03 14:54:54
For example attoparsec's Parser type is a lot of continuations that encodes an algebraic data type.
erisco 2017-02-03 14:55:00
but much more clear if you're intimate with the runtime
jle` 2017-02-03 14:55:05
edwardk gains his speed when he wakes up by using a healthy diet of some good ol' skolemized existentials
erisco 2017-02-03 14:55:32
I mean, what the hey, I'll use this variation just for the fun of it
erisco 2017-02-03 14:55:37
doesn't bother me either way
jle` 2017-02-03 14:55:59
if you're just playing around, the existential constructor might be the conceptually simpler version
monochrom 2017-02-03 14:56:31
Yes. Write a program you actually understand first.
monochrom 2017-02-03 14:56:46
Then transform it for speed until you understand none of it anymore.
monochrom 2017-02-03 14:57:14
That is how to achieve a legacy.
erisco 2017-02-03 14:57:38
I intermingle a bit of known and unknown into my screwing around so that I am learning something ;)
jle` 2017-02-03 14:57:42
i explain some pro's and cons of both styles in the linked article
monochrom 2017-02-03 14:59:32
BTW I hate ACL2 precisely because it doesn't have a native, direct existential, it encodes by the skolemization.
monochrom 2017-02-03 15:00:17
It has the consequence of making existentials second-class. This is a hindrance if I need existentials significantly.
monochrom 2017-02-03 15:00:47
OTOH ACL2's main use case doesn't need existentials, so that's how they do just fine.
erisco 2017-02-03 15:00:54
jle`, wrt the nesting point I find that one a bit weird. I'd be hesitant to format my code like that for CP
erisco 2017-02-03 15:01:05
jle`, and for multiple cases the way to go is guards
jle` 2017-02-03 15:03:18
can you elaborate on which examples you are talking about?
erisco 2017-02-03 15:04:01
https://blog.jle.im/entry/practical-dependent-types-in-haskell-2.html#a-tale-of-two-styles
jle` 2017-02-03 15:04:40
how would you use guards?
jle` 2017-02-03 15:06:03
i've seen nested cp style like that used a lot of codebases and library/application code, but ymmv :)
erisco 2017-02-03 15:09:29
jle`, something like this http://lpaste.net/352071
jle` 2017-02-03 15:10:18
ah, pattern guards
jle` 2017-02-03 15:10:21
um
jle` 2017-02-03 15:10:22
does that work?
erisco 2017-02-03 15:10:27
sure
jle` 2017-02-03 15:10:28
that'd be nice
jle` 2017-02-03 15:12:50
oh hey it works :o
jle` 2017-02-03 15:13:19
might not always be possible to refactor it out as a separate function, though, but i suppose you could just throw in a multi-way if if it's in the middle of an expression
erisco 2017-02-03 15:13:19
I am just hesitant with the CPS notation because I like to use the same formatting regardless of what the content is
jle` 2017-02-03 15:13:45
ty for the tip
jle` 2017-02-03 15:13:55
finally a nice use for pattern guards
erisco 2017-02-03 15:14:04
yeah not sure if you can kick off an anonymous guard
jle` 2017-02-03 15:14:12
you can do it with multi-way if
jle` 2017-02-03 15:14:15
maybe
jle` 2017-02-03 15:16:55
oh yes, it does work
jle` 2017-02-03 15:16:58
but it's kind of awkward
jle` 2017-02-03 15:17:58
indentation for multi-way ifs is different than indentation for normal guards apparently
erisco 2017-02-03 15:25:59
oh I guess the wins really come in because the compiler takes off the newtype and can reduce the applications
erisco 2017-02-03 15:29:06
now this one is puzzling http://lpaste.net/352072
erisco 2017-02-03 15:29:45
happily it seems to know Z is <= to everything
jle` 2017-02-03 15:32:40
erisco: you probably need a proof that forall n. (n :<= n) ~ True
jle` 2017-02-03 15:33:07
type-natural might come with one if you're lucky
jle` 2017-02-03 15:34:29
erisco: yup, it does http://hackage.haskell.org/package/type-natural-0.7.1.2/docs/Data-Type-Natural.html#v:sLeqReflexive
erisco 2017-02-03 15:35:29
lol someone has to standardise these containers... Decision, :~:, Refl, IsTrue
erisco 2017-02-03 15:35:32
too much! :P
jle` 2017-02-03 15:35:47
:~:/Refl are in base
jle` 2017-02-03 15:35:54
Decision is in singletons but it really should be in base i think
jle` 2017-02-03 15:38:56
IsTrue is cute. but '~ True'/definitional equality is kinda weird
jle` 2017-02-03 15:39:01
at this level at least
