TypeNat 0.1.0.0 → 0.2.0.0

raw patch · 2 files changed

+38/−3 lines, 2 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Data/TypeNat/Nat.hs +37/−2
• TypeNat.cabal +1/−1

@@ -1,13 +1,22 @@ {-# LANGUAGE KindSignatures #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE Rank2Types #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE ScopedTypeVariables #-}+-- TBD can we get around incoherent instances!?!+{-# LANGUAGE IncoherentInstances #-}  module Data.TypeNat.Nat (      Nat(..)-  , IsNat-  , natRecursion+  , IsNat(..) +  , LTE(..)++  , Zero   , One   , Two   , Three@@ -23,6 +32,7 @@  data Nat = Z | S Nat +type Zero = Z type One = S Z type Two = S One type Three = S Two@@ -44,3 +54,28 @@  instance IsNat n => IsNat (S n) where   natRecursion ifS ifZ reduce x = ifS x (natRecursion ifS ifZ reduce (reduce x))++-- | 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+  lteRecursion :: (forall k . LTE n k => d (S k) -> d k) -> d m -> d n++instance LTE n n where+  lteInduction f x = x+  lteRecursion f x = x++instance LTE n m => LTE n (S m) where++  lteInduction+    :: forall (d :: Nat -> *) .+       (forall (k :: Nat) . LTE (S k) (S m) => d k -> d (S k))+    -> d n+    -> d (S m)+  lteInduction f x =+      let sub :: d m+          sub = lteInduction f x+      in  f sub++  lteRecursion f x = lteRecursion f (f x)

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                TypeNat-version:             0.1.0.0+version:             0.2.0.0 synopsis:            Some Nat-indexed types for GHC -- description:          homepage:            https://github.com/avieth/TypeNat