It’s really odd that people think pattern matching on types is bad. We get a lot of mileage out of pattern matching on data which encode types, whenever we do a universe construction. If you take the approach that Thorsten Altenkirch and I pioneered (and which my comrades and I began to engineer), the types … Read more
Continuations can be modelled as monads, using CPS, but they are not algebraic effects as they cannot be modelled using Lawvere theories. See Martin Hyland and John Power, 2007, The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads (pdf), ENTCS 172:437-458.
I may not be the best person to answer this, as having implemented Idris I’m probably a bit biased! The FAQ – http://docs.idris-lang.org/en/latest/faq/faq.html – has something to say on it, but to expand on that a bit: Idris has been designed from the ground up to support general purpose programming ahead of theorem proving, and … Read more
Before I answer the main question, I’m going to try to define a bit more precisely what it would mean to write code in Haskell or Idris and compile it to run on an Ethereum-like blockchain. Idris is probably a better fit for this, but I’m going to use Haskell because that’s what I’m familiar … Read more