finite_projectiv 2017-02-18 20:03:49
Here's a fun one liner in haskell
finite_projectiv 2017-02-18 20:03:52
let f1 x = (x,x); f2 = f1 . f1; f3 = f2 . f2; f4 = f3 . f3; f5 = f4 . f4; f6 = f5 . f5 in f6
finite_projectiv 2017-02-18 20:03:56
Run this in a vm btw
finite_projectiv 2017-02-18 20:04:03
Or be ready to kill the process
Koterpillar 2017-02-18 20:10:32
ghc: out of memory
Koterpillar 2017-02-18 20:11:00
(alternate way: ulimit -Sv 1000000)
raynold 2017-02-18 20:13:00
ahh it's a wonderful day
MarcelineVQ 2017-02-18 20:13:06
poor little typechecker :(
ongy 2017-02-18 20:32:57
why does ghc take up so much memory with that one-liner
glguy 2017-02-18 20:33:53
:t let f1 x = (x,x) in f1 -- ; f2 = f1 . f1
lambdabot 2017-02-18 20:33:55
t -> (t, t)
glguy 2017-02-18 20:34:02
:t let f1 x = (x,x); f2 = f1 . f1 in f2
lambdabot 2017-02-18 20:34:05
t -> ((t, t), (t, t))
glguy 2017-02-18 20:34:15
:t let f1 x = (x,x); f2 = f1 . f1; f3 = f2 . f2 in f3
lambdabot 2017-02-18 20:34:17
t -> ((((t, t), (t, t)), ((t, t), (t, t))), (((t, t), (t, t)), ((t, t), (t, t))))
glguy 2017-02-18 20:34:57
:t let f1 x = (x,x); f2 = f1 . f1; f3 = f2 . f2; f4 = f3 . f3 in f4
lambdabot 2017-02-18 20:34:58
t -> ((((((((t, t), (t, t)), ((t, t), (t, t))), (((t, t), (t, t)), ((t, t), (t, t)))), ((((t, t), (t, t)), ((t, t), (t, t))), (((t, t), (t, t)), ((t, t), (t, t))))), (((((t, t), (t, t)), ((t, t), (t,
lambdabot 2017-02-18 20:34:58
t))), (((t, t), (t, t)), ((t, t), (t, t)))), ((((t, t), (t, t)), ((t, t), (t, t))), (((t, t), (t, t)), ((t, t), (t, t)))))), ((((((t, t), (t, t)), ((t, t), (t, t))), (((t, t), (t, t)), ((t, t), (t,
lambdabot 2017-02-18 20:34:58
t)))), ((((t, t), (t, t)), ((t, t), (t, t))), (((t, t), (t, t)), ((t, t), (t, t))))), (((((t, t), (t, t)), ((t, t), (t, t))), (((t, t), (t, t)), ((t, t), (t, t)))), ((((t, t), (t, t)), ((t, t), (t,
lambdabot 2017-02-18 20:34:58
t))), (((t, t), (t, t)), ((t, t), (t, t))))))), (((((((t, t), (t, t)), ((t, t), (t, t))), (((t, t), (t, t)), ((t, t), (t, t)))), ((((t, t), (t, t)), ((t, t), (t, t))), (((t, t), (t, t)), ((t, t), (t,
lambdabot 2017-02-18 20:34:58
t))))), (((((t, t), (t, t)), ((t, t), (t, t))), (((t, t), (t, t)), ((t, t), (t, t)))), ((((t, t), (t, t)), ((t, t), (t, t))), (((t, t), (t, t)), ((t, t), (t, t)))))), ((((((t, t), (t, t)), ((t, t),
lambdabot 2017-02-18 20:35:00
(t, t))), (((t, t), (t, t)), ((t, t), (t, t)))), ((((t, t), (t, t)), ((t, t), (t, t))), (((t, t), (t, t)), ((t, t), (t, t))))), (((((t, t), (t, t)), ((t, t), (t, t))), (((t, t), (t, t)), ((t, t), (t,
lambdabot 2017-02-18 20:35:02
t)))), ((((t, t), (t, t)), ((t, t), (t, t))), (((t, t), (t, t)), ((t, t), (t, t))))))))
shinX 2017-02-18 20:35:14
=_=
glguy 2017-02-18 20:35:19
I didn't expect lambdabot to offer so much output
MP2E 2017-02-18 20:35:28
hah :P
glguy 2017-02-18 20:35:32
In any case, these types grow very quickly
ongy 2017-02-18 20:35:53
they do. That's more than 2^n, wow
ongy 2017-02-18 20:36:23
and good to know that lambdabot doesn't limit the type output
MarcelineVQ 2017-02-18 20:41:31
ongy: related http://spacemanaki.com/blog/2014/08/04/Just-LOOK-at-the-humongous-type/
glguy 2017-02-18 20:42:11
> iterate (2^) 1
lambdabot 2017-02-18 20:42:14
[1,2,4,16,65536,200352993040684646497907235156025575044782547556975141926501...
ongy 2017-02-18 20:44:20
that 6th number looks fine
kadoban 2017-02-18 20:44:44
That sure is a number
