mroman 2017-02-21 09:45:22
Cale: http://codepad.org/WfXlnXJt
Cale 2017-02-21 09:45:57
mroman: Sure...
Cale 2017-02-21 09:46:13
mroman: But you're trying to let the existential escape there.
Cale 2017-02-21 09:46:31
The unsafePerformIO stuff I did there with IORef didn't involve any existentials.
Cale 2017-02-21 09:47:00
also, wtf hugs?
mroman 2017-02-21 09:47:03
I also think undefined is magical.
Tuplanolla 2017-02-21 09:47:14
It's actually not, mroman.
mroman 2017-02-21 09:47:15
it inhabits every type
mroman 2017-02-21 09:47:24
which is weird.
int-e 2017-02-21 09:47:28
so does let x = x in x
mroman 2017-02-21 09:47:42
yeh
nitrix 2017-02-21 09:47:47
mroman: undefined is a bottom value. You could create bottom yourself.
mroman 2017-02-21 09:47:48
I call that magical :D
mroman 2017-02-21 09:48:07
let x = x in x shouldn't even have an assignable type
int-e 2017-02-21 09:48:16
It's just lazy?
Tuplanolla 2017-02-21 09:48:23
Magical usually means something you couldn't define yourself, mroman.
nitrix 2017-02-21 09:48:23
mroman: The type system (and the whole design of Haskell) actually accomodates and takes into account bottoms in its specification, as well as proofs.
mroman 2017-02-21 09:48:48
Tuplanolla: Obviously magical here means "I don't understand it" ;)
Tuplanolla 2017-02-21 09:49:01
Well, then all bets are off.
mroman 2017-02-21 09:49:54
and in the type system I have in my head let x = x in x doesn't have an assignable type.
mroman 2017-02-21 09:50:10
that's like writing def foo(): return foo();
nitrix 2017-02-21 09:50:12
mroman: forall t. t
Tuplanolla 2017-02-21 09:50:19
I bet you'd enjoy Gallina (Coq), mroman.
nitrix 2017-02-21 09:50:31
mroman: For every type `t`, we're at value of type `t`.
int-e 2017-02-21 09:50:34
mroman: what about template T f() { return f(); } in C++ ;-)
nitrix 2017-02-21 09:50:42
mroman: *that
nitrix 2017-02-21 09:51:00
mroman: It represents very nicely what the expression does.
int-e 2017-02-21 09:51:05
mroman: granted that doesn't inhabit every type, but it can be instantiated for any type.
nitrix 2017-02-21 09:51:07
mroman: Polymorphism for every `t`.
int-e 2017-02-21 09:51:33
(the lesson here is that strict languages have bottoms too)
int-e 2017-02-21 09:51:56
(as long as they don't ensure termination)
mroman 2017-02-21 09:52:02
I think there's already a nice quote which states my opinion of bottoms.
mroman 2017-02-21 09:52:36
I refuse to believe in them.
kadoban 2017-02-21 09:52:43
Is it a sir mixalot quote?
mroman 2017-02-21 09:53:11
I'm a hardcore finetist.
mroman 2017-02-21 09:53:15
or whatever that's called.
mroman 2017-02-21 09:53:23
*finitetist
Tuplanolla 2017-02-21 09:54:33
Finitist, no?
mroman 2017-02-21 09:54:57
That seems to be the correct spelling, yes.
mroman 2017-02-21 09:55:09
Goes without saying I refuse the halting problem.
Tuplanolla 2017-02-21 09:55:43
Too bad all the interesting things are at least countable.
nitrix 2017-02-21 09:55:45
It's a good attitude. Some people have designed languages that are guaranteed to halt.
nitrix 2017-02-21 09:55:51
It's very useful for theorem proving.
mroman 2017-02-21 09:56:12
Mainly because I haven't found a proof yet that doesn't rely on magic.
Tuplanolla 2017-02-21 09:56:39
Thus my remark about Coq, mroman.
nitrix 2017-02-21 09:56:45
You keep calling universal quantification "magic".
nitrix 2017-02-21 09:57:18
mroman: May I ask what confuses you with `forall t. t` ?
mroman 2017-02-21 10:00:16
Can I read that as "forall t. I return t"?
mroman 2017-02-21 10:01:54
Tuplanolla: well the problem with the "sketch proofs" is that they feed something to itself
mroman 2017-02-21 10:02:07
which wouldn't properly type check.
nitrix 2017-02-21 10:02:10
mroman: First, there is no `->` so what you're working with isn't a function that'd take arguments.
nitrix 2017-02-21 10:02:11
mroman: It merely is a value. A polymorphic value at that. It's type is `t`, where we introduced `t` to be all types.
mroman 2017-02-21 10:02:45
That assumes the existence of values that are members of an infinite amount of types.
nitrix 2017-02-21 10:03:09
mroman: So it doesn't "return" really. It's an inhabitant of all types.
mroman 2017-02-21 10:03:13
I don't even believe in values being member of multiple types.
mroman 2017-02-21 10:03:55
if it doesn't return
mroman 2017-02-21 10:03:59
then what's it's value?
mroman 2017-02-21 10:04:08
*its
nitrix 2017-02-21 10:04:19
It doesn't _have_ a value. It _is_ a value.
mroman 2017-02-21 10:04:50
I see.
mroman 2017-02-21 10:05:03
so undefined :: forall t. t?
nitrix 2017-02-21 10:05:09
:t undefined
lambdabot 2017-02-21 10:05:12
a
nitrix 2017-02-21 10:05:22
Correct.
mroman 2017-02-21 10:05:31
is undefined == undefined?
mroman 2017-02-21 10:05:44
or undefined == 5?
dolio 2017-02-21 10:05:45
What is ==?
mroman 2017-02-21 10:05:53
comparison
Tuplanolla 2017-02-21 10:06:12
Choose your equality: https://ncatlab.org/nlab/show/equality
nitrix 2017-02-21 10:06:13
mroman: No, because not all types allows you to compare for equality.
dolio 2017-02-21 10:06:22
Then no.
mroman 2017-02-21 10:06:30
undefined == 5 aborts with an error.
mroman 2017-02-21 10:06:37
which I consider to be an incredibly bad design choice.
nitrix 2017-02-21 10:06:39
mroman: But I guaranteed you `id undefined = undefined`, that is, its identity can be preserved.
mroman 2017-02-21 10:06:46
it means that foo a b = a == b is UNSAFE
nitrix 2017-02-21 10:07:20
mroman: The decision behind making undefined terminate the program is by choice.
dolio 2017-02-21 10:07:46
undefined is an 'abort with an error'.
nitrix 2017-02-21 10:08:15
mroman: A different implementation of undefined could just make the program hang, trying to compute a value it cannot compute, and then, it'd be "safe" by any consideration.
nitrix 2017-02-21 10:08:42
mroman: What you're describing is merely the essence of _|_ (bottom). `undefined` is a design choice for convenience.
dolio 2017-02-21 10:09:36
Being able to detect undefined is actually the bad design.
mroman 2017-02-21 10:09:53
well... letting undefined hang forever would be worse
dolio 2017-02-21 10:09:55
Because that makes it the equivalent of null.
mroman 2017-02-21 10:10:57
I'd prefer null.
nitrix 2017-02-21 10:11:05
mroman: But as far as the limited examples you provided, undefined == undefined is a type error.
mroman 2017-02-21 10:11:24
:t undefined == undefined
mroman 2017-02-21 10:11:26
no it's not.
lambdabot 2017-02-21 10:11:26
Bool
mroman 2017-02-21 10:11:39
not to haskell at least.
dolio 2017-02-21 10:12:21
Not in GHC with extended default rules.
dolio 2017-02-21 10:12:29
It'd be a type error in Haskell.
mroman 2017-02-21 10:12:45
because can't deduce that t is Eq
mroman 2017-02-21 10:12:50
I presume?
dolio 2017-02-21 10:13:17
It can't decide which Eq instance to use.
mroman 2017-02-21 10:13:18
although if it inhabits any type wouldn't it inhabit every type class as well?
kadoban 2017-02-21 10:13:21
Because it has no way to know what instance of t you want, and has no defaulting rules to pick one for you.
Tuplanolla 2017-02-21 10:13:34
What's the lens way to perform `insertWith`? I'd like to only insert a value if it's not present.
kadoban 2017-02-21 10:13:51
s/instance of t/instance of Eq/
mroman 2017-02-21 10:13:57
but ok
mroman 2017-02-21 10:14:30
but why can't I create an IORef a and break the type system without unsafePerformIO?
dolio 2017-02-21 10:15:22
Because breaking the type system relies on let generalization.
dolio 2017-02-21 10:15:55
To use the same reference at multiple types.
mroman 2017-02-21 10:17:59
let generalizations.
mroman 2017-02-21 10:18:02
my todo list just grew :D
mroman 2017-02-21 10:19:36
int-e: T f() { return f(); } is fine btw.
mroman 2017-02-21 10:19:55
because it defines f to have a return type T
mroman 2017-02-21 10:20:17
but infering f() { return f(); } is something different.
sternmull 2017-02-21 10:20:18
i want to call a STM () inside a IO ()... what do i have to do? Probably one of the lifts.
mroman 2017-02-21 10:20:24
that's not possible.
exio4 2017-02-21 10:20:27
:t let f () = f () in f
lambdabot 2017-02-21 10:20:30
() -> t
mroman 2017-02-21 10:20:31
except in haskell maybe :D
exio4 2017-02-21 10:20:35
sternmull: atomically!
fresheyeball 2017-02-21 10:20:52
anyone out there know how to serve gzipped files with Servant?
int-e 2017-02-21 10:21:17
mroman: Well, ML too. Which probably extends to all the other typed functional programming languages.
mroman 2017-02-21 10:21:23
in some type systems inference is impossible
int-e 2017-02-21 10:21:34
(That don't mandate totality)
mroman 2017-02-21 10:21:35
unless type annotations are given.
sternmull 2017-02-21 10:21:36
exio4: Oh.. would never had figured that out on myself. Thank you.
mroman 2017-02-21 10:22:33
is there even another way to construct forall t. t except doing infinite recursion?
ertes 2017-02-21 10:22:45
helo
exio4 2017-02-21 10:22:54
mroman: in Haskell?
lyxia 2017-02-21 10:22:59
throw an exception
mroman 2017-02-21 10:23:09
in a haskell-y type system
exio4 2017-02-21 10:23:09
mroman: exceptions in pure code are a bottom too
lyxia 2017-02-21 10:24:02
there's nothing more Haskell-y than Haskell.
nitrix 2017-02-21 10:24:54
Speaking of which, can someone explain to me why this is possible?
nitrix 2017-02-21 10:25:04
let x = 1 : [length x] ?
Tuplanolla 2017-02-21 10:25:35
> let x = 1 : [length x] in x
lambdabot 2017-02-21 10:25:39
[1,2]
Cale 2017-02-21 10:25:46
nitrix: Well, what prevents it from working? :)
nitrix 2017-02-21 10:25:52
Nevermind, wrong example.
nitrix 2017-02-21 10:25:57
That one works because of lazyness.
Cale 2017-02-21 10:26:01
length doesn't care about the actual elements of the list, right
bollu 2017-02-21 10:26:17
what does ~(a, b) do?
nitrix 2017-02-21 10:26:21
I had a funkier case today.
bollu 2017-02-21 10:26:21
it's a little hard to google
nitrix 2017-02-21 10:26:24
Trying to find it.
Cale 2017-02-21 10:26:27
bollu: That's a lazy pattern match
bollu 2017-02-21 10:26:35
Cale: oh, that exists?
fresheyeball 2017-02-21 10:26:40
anyone know if serveDirectory serves gzip files?
Cale 2017-02-21 10:26:42
bollu: It will succeed without doing any evaluation
bollu 2017-02-21 10:26:49
Cale: in the sense?
Cale 2017-02-21 10:26:55
bollu: and only evaluate the argument if x or y needs to be evaluated
Cale 2017-02-21 10:27:08
With pairs, it's safe
Cale 2017-02-21 10:27:30
With types that have multiple constructors, be a bit careful, because you'll get an error if the pattern doesn't actually match
bollu 2017-02-21 10:27:46
Cale: can you show me an example of you using it?
Cale 2017-02-21 10:27:46
> case Nothing of ~(Just x) -> 5
lambdabot 2017-02-21 10:27:51
5
bollu 2017-02-21 10:27:55
what? o_O
bollu 2017-02-21 10:28:00
OK
Cale 2017-02-21 10:28:01
^^ but only if you actually use the variable
Cale 2017-02-21 10:28:04
> case Nothing of ~(Just x) -> x
lambdabot 2017-02-21 10:28:10
*Exception: :(3,1)-(4,22): Irrefutable pattern failed for patte...
bollu 2017-02-21 10:28:31
Cale: I don't understand, why did it match with ~(Just x) ?
bollu 2017-02-21 10:28:35
does it always succeed
bollu 2017-02-21 10:28:36
?
Cale 2017-02-21 10:28:40
yes
exio4 2017-02-21 10:28:40
a lazy pattern match always succeeds
bollu 2017-02-21 10:28:44
I see
exio4 2017-02-21 10:28:54
the error happens when you *use* a variable, not when you match
bollu 2017-02-21 10:28:59
> case undefined of ~(1, 1) -> 4
lambdabot 2017-02-21 10:29:02
4
Tuplanolla 2017-02-21 10:29:04
It's mostly useful for single-constructor values, bollu.
bollu 2017-02-21 10:29:04
wow
mroman 2017-02-21 10:29:20
witchcraft.
Cale 2017-02-21 10:29:24
For ~(x,y)
bollu 2017-02-21 10:29:27
Tuplanolla: I found a comment in the GHC source: mfix (\ ~(a,b,c) -> do ...; return (a',b',c'))
bollu 2017-02-21 10:29:35
so, like, why would you want a ~(a, b, c)?
Cale 2017-02-21 10:29:38
it's the same as if you wrote let x = fst p; y = snd p in ...
bollu 2017-02-21 10:29:44
I see
bollu 2017-02-21 10:29:50
till you use it, it is never used
bollu 2017-02-21 10:30:37
> case undefined of (x, y) -> 5
johnw 2017-02-21 10:31:37
it's a thunk that only deconstructs the value when the result is demanded
mroman 2017-02-21 10:39:17
exio4: yes...?
exio4 2017-02-21 10:39:29
mroman: undefined represents a ⊥, it's not directly related to nullable types
nil_ 2017-02-21 10:39:49
mroman: my point is, it's not really a "choice" at all. Bottom is what it is, you don't get to design its behaviour.
exio4 2017-02-21 10:39:51
mroman: it's a result of having a turing-complete non-strict programming language
mroman 2017-02-21 10:40:13
I'm pretty sure you could get that without bottom too
mroman 2017-02-21 10:40:17
but I can never proof it.
exio4 2017-02-21 10:40:26
mroman: nullable types are akin to having a value you can "pattern match on" for every value
mroman 2017-02-21 10:40:56
yes. because nullable types might have a value or a non-value
ph88^ 2017-02-21 10:41:01
does anyone know how to enable the optimal compiler algorithm for ApplicativeDo ?
Tuplanolla 2017-02-21 10:41:18
It's probably related to Day convolution, which I know nothing about, mroman.
bollu 2017-02-21 10:41:29
mroman: from what little I understand, there is an operation called Day Convolution, which lets one express Applicative as "monoid of endofunctors" with "compostition" being "Day convolution"
Tuplanolla 2017-02-21 10:41:48
I see I'm not alone on this.
mroman 2017-02-21 10:42:15
exio4: undefined is used for "NotImplemented" stuff.
mroman 2017-02-21 10:42:17
which is uhm..
mroman 2017-02-21 10:42:20
mostly bad anyway
MarcelineVQ 2017-02-21 10:42:45
ph88^: same way as any other extension, ApplicativeDo is picky about your notation though, don't end your do block with something like return $ foo 3 bur rather return (foo 3)
exio4 2017-02-21 10:42:46
mroman: undefined is ⊥, I don't get what you mean?
nil_ 2017-02-21 10:43:05
dolio has also pointed out that allowing you to *catch* errors /is/ a design decision and a bad one at that.
fresheyeball 2017-02-21 10:43:15
exio4: undefined is an absurd type
MarcelineVQ 2017-02-21 10:43:16
ph88^: Though, I read that as optional, if you meant optimal then I'm not sure what you mean
fresheyeball 2017-02-21 10:43:18
:t undefined
exio4 2017-02-21 10:43:21
fresheyeball: it's a value
lambdabot 2017-02-21 10:43:21
a
fresheyeball 2017-02-21 10:43:38
exio4: sorry, I mean undefined HAS an absurd type
exio4 2017-02-21 10:43:59
fresheyeball: well, ⊥ has an nonsense type :)
fresheyeball 2017-02-21 10:44:00
undefined :: forall a. a
exio4 2017-02-21 10:44:07
fresheyeball: it's one of the issues of being turing-complete
ph88^ 2017-02-21 10:44:13
MarcelineVQ, really it can't handle $ in return ? wow :|
ph88^ 2017-02-21 10:44:17
i use that EVERYWHERE
fresheyeball 2017-02-21 10:44:32
undefined is really good for development workflow
exio4 2017-02-21 10:44:34
fresheyeball: in a "normal" strict programming language you might still have nonsense values too
fresheyeball 2017-02-21 10:44:46
exio4: yes this is true
exio4 2017-02-21 10:44:54
template T f() { return f(); } -- like given earlier, it's a "nonsense" function
ph88^ 2017-02-21 10:44:58
MarcelineVQ, in the ICFP 2016 talk about it they say you can choose a heuristic search that O^2 and an optimal search that's O^3 .. so your compilation is slower but you get the best results
exio4 2017-02-21 10:45:02
that works in ML too, which is a functional and strict language
ph88^ 2017-02-21 10:45:09
hi fresheyeball
