3 ms·

GHC Haskell type-level Integer literals can constructed from non-literal just fine :) https://hackage.haskell.org/package/base-4.7.0.2/docs/GHC-TypeLits.html#

GHC Haskell type-level Integer literals can constructed from non-literal just fine :) https://hackage.haskell.org/package/base-4.7.0.2/docs/GHC-TypeLits.html#v:someNatVal https://hackage.haskell.org/package/base-4.7.0.2/docs/GHC-Ty... There are type-level operators as well for arithmetic, but in my experience it’s a bit less pleasant than working with Peano Nats.

pron 9y ago
And can you say that a type is indexed by, say, an even number? How do you prove that?
- catnaroek 9y ago
  A 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 ago
  With 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.