I love the Idris developments, but this thread gives a different perspective and gives interesting critiques.https://twitter.com/pressron/status/1115575346315841537 …
-
-
I think what's cool is what is achievable in this type system with what is essentially an ad-hoc weekend hack. If we learn to use types more effectively, there's so much more we could do! I think this will start to be really effective with, e.g., implementing complex protocols.
-
Yeah, that's the impression I've gotten from your talks: More about this kind of thing being within reach, without reaching *very* far. Less about the actual trick.
- 5 more replies
New conversation -
-
-
I might have not phrased myself in the best way, I referred to his general comparison of model theory to proof theory, coming myself mostly from proofs and types.
-
Sure, it's always good to look at these things from other people's perspectives. None of us have the definitive answers after all!
- 2 more replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.