wiki:TypeNats/SingletonsAndExistentials

Version 1 (modified by diatchki, 2 years ago) (diff)

--

Consider a type for arrays with a statically known size.

newtype StaticArray (n :: Nat) a = SA (Ptr a)
data ArrayS :: * -> * where
  ArrS :: Sing n -> StaticArray n a -> ArrayS a
data ArrayD :: * -> * where
  ArrD :: SingI n => StaticArray n a -> ArrayD a