Changes between Version 1 and Version 2 of TypeNats/SingletonsAndExistentials


Ignore:
Timestamp:
Apr 17, 2012 8:02:24 PM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/SingletonsAndExistentials

    v1 v2  
    11Consider a type for arrays with a statically known size.
    22{{{
    3 newtype StaticArray (n :: Nat) a = SA (Ptr a)
     3newtype ArrPtr (n :: Nat) a = SA (Ptr a)
    44}}}
    55
     
    77{{{
    88data ArrayS :: * -> * where
    9   ArrS :: Sing n -> StaticArray n a -> ArrayS a
     9  ArrS :: Sing n -> ArrPtr n a -> ArrayS a
    1010}}}
    1111
    1212{{{
    1313data ArrayD :: * -> * where
    14   ArrD :: SingI n => StaticArray n a -> ArrayD a
     14  ArrD :: SingI n => ArrPtr n a -> ArrayD a
    1515}}}