modal types, generalized arrows, and core passes written in coq
megacz at cs.berkeley.edu
Sun Mar 13 19:59:10 CET 2011
Max Bolingbroke <batterseapower at hotmail.com> writes:
> $ ~/Programming/Checkouts/ghc-garrows/inplace/bin/ghc-stage2
> -ddump-types GArrows-Pow.hs -dcoqpass -fforce-recomp
> What am I doing wrong?
You're still using -dcoqpass, which I asked you not to use on tutorial.hs:
> I'm not sure what you mean by HelloWorld - it doesn't seem to be
> mentioned on that page.
Search for "HelloWorld" in: http://www.cs.berkeley.edu/~megacz/coq-in-ghc/
> instance GArrow (->) (,) where
FWIW, this is just the Control.Arrow instance for (->) taken as a GArrow
via this instance:
> This doesn't compile because the "flatten" function you claim is
> exported from GHC.HetMet.CodeTypes doesn't exist.
It will be posted tomorrow. Except for the fact that the git repo
for the base library is broken:
... so actually it will be posted whenever that gets fixed. Development
is basically halted until then.
> You need
> <[ (*) ]> :: forall a. <[ Int -> Int -> Int ]>@a
> And you also need something like this declaration:
> <[ fromInteger ]> :: forall a. <[ Integer -> Int ]>@a
Thanks; typos fixed.
More information about the Cvs-ghc