4 ms·
And can you say that a type is indexed by, say, an even number? How do you prove that?
by pron 9y ago
And can you say that a type is indexed by, say, an even number? How do you prove that?
- catnaroek 9y agoA dependent type system needn't be able to express that a type is indexed by an even number. You can have dependent types without type-level computation, for example, by requiring that types be parameterized by nonexpansive expressions - which is nevertheless already more powerful than what Haskell's type system offers. This restriction might even be a good thing for type inference.
- whateveracct 9y agoWith TypeLits, idk if that’s possible without some cheating. But that’s because (as the module name implies) these are type literals and mostly focused on having Integers that can go from type to term and vice-versa. I can definitely do that with Singleton peano Nats pretty easily. I’ll end up with a function of type SNat n -> Maybe (IsEven n) Where IsEven n is some structural proof of even-ness data IsEven (n :: Nat) where ZEven :: IsEven Z SEven :: forall (n ::Nat). IsEven n -> IsEven (S (S n)) I wrote this on my phone, but I’m sure it’s possible and kinda easy to work with at that.