TypeNat 0.2.1.0 → 0.4.0.0

raw patch · 3 files changed

+57/−13 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Data/TypeNat/Nat.hs +38/−10
• Data/TypeNat/Vect.hs +4/−0
• TypeNat.cabal +15/−3

@@ -1,12 +1,13 @@ {-# LANGUAGE KindSignatures #-} {-# LANGUAGE DataKinds #-}-{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-}--- TBD can we get around incoherent instances!?! {-# LANGUAGE IncoherentInstances #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE TypeFamilies #-}  module Data.TypeNat.Nat ( @@ -14,6 +15,7 @@   , IsNat(..)    , LTE(..)+  , StrongLTE    , Zero   , One@@ -29,8 +31,22 @@    ) where +import Data.Proxy+import GHC.Exts (Constraint)+ data Nat = Z | S Nat +instance Eq Nat where+    Z == Z = True+    (S n) == (S m) = n == m+    _ == _ = False++instance Ord Nat where+    Z `compare` Z = EQ+    S n `compare` S m = n `compare` m+    S n `compare` Z = GT+    Z `compare` S m = LT+ type Zero = Z type One = S Z type Two = S One@@ -54,22 +70,34 @@ instance IsNat n => IsNat (S n) where   natRecursion ifS ifZ reduce x = ifS x (natRecursion ifS ifZ reduce (reduce x)) +-- | A constrint which includes LTE k m for every k <= m.+type family StrongLTE (n :: Nat) (m :: Nat) :: Constraint where+  StrongLTE Z m = LTE Z m+  StrongLTE (S n) m = (LTE (S n) m, StrongLTE n m)+ -- | Nat @n@ is less than or equal to nat @m@. --   Comes with functions to do type-directed computation for Nat-indexed --   datatypes. class LTE (n :: Nat) (m :: Nat) where-  lteInduction :: (forall k . LTE (S k) m => d k -> d (S k)) -> d n -> d m+  lteInduction+    :: StrongLTE m l+    => Proxy l+    -> (forall k . LTE (S k) l => d k -> d (S k))+    -- ^ The parameter l is fixed by any call to lteInduction, but due to+    --   the StrongLTE m l constraint, we have LTE j l for every j <= m.+    --   This allows us to implement the nontrivial case in the+    --     @LTE p q => LTE p (S q)@+    --   instance, where we need to use this function to get @x :: d p@ and then+    --   again to get @f x :: d (S p)@. So long as @p@ and @S p@ are both+    --   less or equal to @l@, this can be done.+    -> d n+    -> d m   lteRecursion :: (forall k . LTE n k => d (S k) -> d k) -> d m -> d n  instance LTE n n where-  lteInduction f x = x+  lteInduction _ f x = x   lteRecursion f x = x  instance LTE n m => LTE n (S m) where--  -- Use the LTE n m instance to get  lteInduction f x :: d m-  -- With this in hand, we can apply f again because-  -- LTE (S m) (S m) is true so that f :: d m -> d (S m) and we're there!-  lteInduction f x = f (lteInduction f x)-+  lteInduction (proxy :: Proxy l) f (x :: d n) = f (lteInduction proxy f x)   lteRecursion f x = lteRecursion f (f x)

@@ -1,6 +1,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE StandaloneDeriving #-}  module Data.TypeNat.Vect ( @@ -22,6 +23,9 @@ data Vect :: * -> Nat -> * where   VNil :: Vect a Z   VCons :: a -> Vect a n -> Vect a (S n)++deriving instance Eq t => Eq (Vect t n)+deriving instance Show t => Show (Vect t n)  -- | A kind of fmap for Vect. vectMap :: (a -> b) -> Vect a n -> Vect b n

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                TypeNat-version:             0.2.1.0+version:             0.4.0.0 synopsis:            Some Nat-indexed types for GHC -- description:          homepage:            https://github.com/avieth/TypeNat@@ -18,7 +18,19 @@ library   exposed-modules:     Data.TypeNat.Fin, Data.TypeNat.Nat, Data.TypeNat.Vect   -- other-modules:       -  other-extensions:    DataKinds, KindSignatures, GADTs, Rank2Types-  build-depends:       base >=4.7 && <4.8+  other-extensions:    DataKinds+                     , KindSignatures+                     , GADTs+                     , RankNTypes+                     , MultiParamTypeClasses+                     , FlexibleInstances+                     , FlexibleContexts+                     , ScopedTypeVariables+                     , IncoherentInstances+                     , ConstraintKinds+                     , TypeFamilies+                     , KindSignatures++  build-depends:       base >=4.7 && < 4.8   -- hs-source-dirs:         default-language:    Haskell2010