3 ms·
Very cool! This might be a naive question. Are your arithmetic patterns equivalent to dependent types, like those found in Idris?
by slewis 4y ago
Very cool! This might be a naive question. Are your arithmetic patterns equivalent to dependent types, like those found in Idris?
- zesterer 4y agoThey're more akin to 'destructuring' natural numbers into successors. Consider: data Nat = Zero | Succ Nat You could pattern match on this Nat, fetching the inner Nat, allowing the type system to prove that all cases are handled exhaustively. Arithmetic patterns just extend this notion to the built-in Nat type. Full dependent typing is something I'd like to experiment with in time, but I'm not there yet.