Axman6 2017-02-03 15:47:57
@hoogle ForeignPtr Word8 -> Int -> IO ByteString
lambdabot 2017-02-03 15:48:01
GHC.Conc runHandlers :: ForeignPtr Word8 -> Signal -> IO ()
lambdabot 2017-02-03 15:48:01
GHC.Conc.Signal runHandlers :: ForeignPtr Word8 -> Signal -> IO ()
lambdabot 2017-02-03 15:48:01
FastString mkFastStringForeignPtr :: Ptr Word8 -> ForeignPtr Word8 -> Int -> IO FastString
riaqn 2017-02-03 15:48:32
Hi, how is closure implemented in GHC? Does the whole stack frame got copied into a new allocated chunk?
Axman6 2017-02-03 15:49:32
the stack in Haskell is not a stack as you know it, importantly it is not use for function calls and returns
Axman6 2017-02-03 15:49:58
look for papers by Simon Peyton-Jones on the STG, Spineless, Tagless G-machine
Axman6 2017-02-03 15:50:14
(I should say, thet stack in GHC, other compilers may use other techniques)
riaqn 2017-02-03 15:50:46
Axman6: OK, thanks!
erisco 2017-02-03 15:53:04
Module `Data.Type.Natural' does not export `sLeqReflexive' what curse is this
erisco 2017-02-03 15:54:08
seems I have to update... weird I just installed it a few days ago
erisco 2017-02-03 15:56:56
oh, damn, that was the issue...
erisco 2017-02-03 15:57:10
sized-vector has the dependency set on 0.4.2.0
erisco 2017-02-03 15:57:30
and now cabal has installed a newer version of type-natural and now sized-vector doesn't work... why does cabal do this
erisco 2017-02-03 15:57:47
any other sized vectors I can use? :s
erisco 2017-02-03 15:59:42
apparently it was a deprecated package to begin with
schoppenhauer 2017-02-03 16:00:06
hi. is it possible to dump the generated STGM-code that ghc generates while compiling?
erisco 2017-02-03 16:00:12
and they did that thing I don't like... they generalised it
erisco 2017-02-03 16:00:25
now I have to use Sized which has gems such as ListLike? oh boy
geekosaur 2017-02-03 16:03:33
schoppenhauer, -ddump-stg
erisco 2017-02-03 16:03:42
when writing the new generalised shiny version do me a favour and also write the specialised functions to mimic the old one
erisco 2017-02-03 16:04:04
import Data.Sized.ForDummies
schoppenhauer 2017-02-03 16:05:03
geekosaur: thx
riaqn 2017-02-03 16:09:14
Axman6: so in SPJ92, 9.4.1, he mentioned that the local environment has to be saved.
riaqn 2017-02-03 16:09:30
but I'm not sure what he means by "save in the stacks"
erisco 2017-02-03 16:10:25
lol the hilarity of doing simple things when you need to prove them
Axman6 2017-02-03 16:10:28
me either, I haven't read it :)
riaqn 2017-02-03 16:10:56
Axman6: I assume it's the stacks allocated in heap.
erisco 2017-02-03 16:11:07
one does not simply subtract 1 from a natural
erisco 2017-02-03 16:14:05
need to get from a < b to there is a predecessor to b, c, and a <= c
erisco 2017-02-03 16:16:26
so one browses through the zoo of axioms and theorems and tries to concoct this fact
mniip 2017-02-03 16:19:02
erisco, are a,b reals?
erisco 2017-02-03 16:19:08
naturals
erisco 2017-02-03 16:19:31
lneqRightPredSucc is probably involved
mniip 2017-02-03 16:19:34
hmm
erisco 2017-02-03 16:19:40
this brings me back to logic class in uni...
erisco 2017-02-03 16:19:52
spend 4 hours trying to find the magical step
mniip 2017-02-03 16:20:28
b is either 0 or has a predecessor, if b=0 then existence of a proves falsehood
erisco 2017-02-03 16:20:56
a < b is true, that is assumed
mniip 2017-02-03 16:21:05
right
mniip 2017-02-03 16:21:18
but surely,
mniip 2017-02-03 16:21:22
a < 0 => falso
erisco 2017-02-03 16:23:28
lneqRightPredSucc gives me b :~: Succ (Pred b)
erisco 2017-02-03 16:23:39
so I've got that b has a predecessor
erisco 2017-02-03 16:25:02
lneqSuccLeq then gives me Succ a :<= Succ (Pred b)
erisco 2017-02-03 16:25:12
where is the Succ peeler!
erisco 2017-02-03 16:26:19
leqSucc adds a Succ
erisco 2017-02-03 16:28:25
jle`, there is leqRefl :: Sing (n :: nat) -> IsTrue (n :<= n) btw
erisco 2017-02-03 16:28:41
rather than the longer sLeqReflexive a a (reflToSEqual a a Refl)
erisco 2017-02-03 16:31:13
hm, I can piece together the Succ elimination from leqSuccStepR (adds Succ to the right) and leqTrans and leqRefl
erisco 2017-02-03 16:32:54
would be nicer to have a lemma for any two naturals though
erisco 2017-02-03 16:37:28
there is addition elimination
patbecich 2017-02-03 16:40:10
/msg NickServ VERIFY REGISTER patbecich lwadzlhxtxzg
patbecich 2017-02-03 16:40:10
MarcelineVQ 2017-02-03 16:40:32
:>
