3 ms·

Thanks for pointing out the Conal Elliott talk. Just watched it, very nice talk. I found myself nodding to pretty much everything he said, except of his fondnes

Thanks for pointing out the Conal Elliott talk. Just watched it, very nice talk. I found myself nodding to pretty much everything he said, except of his fondness for dependent types. Each time he says "dependent types", I just replace it in my mind with "logic". I think he will transition eventually: Types (Haskell) -> Dependent Types (Agda) -> Logic (Practal), hehehe.

agentultra 3y ago
Well you can encode any logic you want in dependent types, so yeah probably!
- practal 3y ago
  Fair enough. Although to encode a proposition as a type, only to then view it as a proposition again, would be two wrappers too many for my taste. I prefer to keep the notions of truth and types apart. In practice, this makes the logic both simpler and more expressive.