search

compiling-to-categories / concat

Compiling to Categories
http://conal.net/papers/compiling-to-categories
BSD 3-Clause "New" or "Revised" License
431 stars 49 forks source link

Compiling to categories with dependent types #110

Open conal opened 1 year ago

conal commented 1 year ago

Haskell’s and GHC Core’s type systems impose severe limitations on the expressiveness of compiling to categories, including (but not only) the inability to express and verify the semantic correctness that lies just beneath the surface (homomorphic specifications and reasoning).

I have moved my category-based work over to Agda, where I’m able to address many more examples and verify their full correctness (not just properties). If anyone is interested in helping & playing, please let me know.

JordanMartinez commented 1 year ago

I'm watching this repo mainly to stay updated on how this experiment is going. I don't plan to contribute. Will the new Agda-based work be done in a new repository or here? If a new one, I'd like to watch that repository and stop watching this one.

conal commented 1 year ago

I'm watching this repo mainly to stay updated on how this experiment is going. I don't plan to contribute. Will the new Agda-based work be done in a new repository or here? If a new one, I'd like to watch that repository and stop watching this one.

Elsewhere, but the location is in flux.