4 ms·
More on how much GHC (and other compilers) can reason about resources (alternatively:infer/thorem prove from type signatures and knowledge about data structures
by gtani 14y ago
More on how much GHC (and other compilers) can reason about resources (alternatively:infer/thorem prove from type signatures and knowledge about data structures used:
http://stackoverflow.com/questions/11725899/is-there-a-theory-that-combines-category-theory-abstract-algebra-and-computation http://stackoverflow.com/questions/11725899/is-there-a-theor...
http://homepages.inf.ed.ac.uk/bcampbe2/thesis/thesis-final.pdf http://homepages.inf.ed.ac.uk/bcampbe2/thesis/thesis-final.p...
http://research-repository.st-andrews.ac.uk/bitstream/10023/564/6/Pedro%20B%20Vasconcelos%20PhD%20thesis.pdf http://research-repository.st-andrews.ac.uk/bitstream/10023/...
http://www.cs.cmu.edu/~rwh/papers/iolambda/short.pdf http://www.cs.cmu.edu/~rwh/papers/iolambda/short.pdf
Also, there's djinn
- dbaupp 14y agoDjinn: "I've written a small program that takes a (Haskell) type and gives you back a function of that type if one exists." ("cabal install djinn" works to install it.) http://lambda-the-ultimate.org/node/1178 http://lambda-the-ultimate.org/node/1178
- gtani 14y agoThx, I was looking for a ref: http://www.polyomino.f2s.com/david/haskell/programsfromproofs.html http://www.polyomino.f2s.com/david/haskell/programsfromproof...
- ky3 14y agoDon't you want there to be a big warning sign that your references are to bleeding edge academic literature that are NOT implemented in GHC and simply aren't in the works at all?