type-unary 0.2.8 → 0.2.13

raw patch · 4 files changed

+22/−9 lines, 4 filesdep ~ty

Dependency ranges changed: ty

Files

• src/TypeUnary/Nat.hs +6/−1
• src/TypeUnary/TyNat.hs +4/−2
• src/TypeUnary/Vec.hs +8/−3
• type-unary.cabal +4/−3

@@ -35,6 +35,7 @@  import Control.Applicative ((<$>)) import Data.Maybe (isJust)+import Data.Typeable (Typeable)  import Data.Proof.EQ @@ -269,6 +270,7 @@   (*)    = noIndex "(*)"   abs    = noIndex "abs"   signum = noIndex "signum"+  negate = noIndex "negate"  noIndex :: String -> a noIndex meth = error (meth ++ ": no method for Index n. Sorry.")@@ -281,7 +283,10 @@ --------------------------------------------------------------------}  -- | Is @n@ a natural number type?-class IsNat n where nat :: Nat n+class Typeable n => IsNat n where nat :: Nat n  instance            IsNat Z     where nat = Zero instance IsNat n => IsNat (S n) where nat = Succ nat++-- The Typeable superclass enables client code to deduce Typeable from IsNat.+-- Occasionally useful.

@@ -1,5 +1,6 @@ {-# LANGUAGE TypeFamilies, TypeOperators, EmptyDataDecls #-} {-# LANGUAGE UndecidableInstances #-} -- for :*:+{-# LANGUAGE DeriveDataTypeable #-} {-# OPTIONS_GHC -Wall #-} ---------------------------------------------------------------------- -- |@@ -20,11 +21,12 @@   , N0,N1,N2,N3,N4,N5,N6,N7,N8,N9,N10,N11,N12,N13,N14,N15,N16   ) where +import Data.Typeable (Typeable)  -- | Type-level representation of zero-data Z+data Z    deriving Typeable -- | Type-level representation of successor-data S n+data S n  deriving Typeable  -- INSTANCE_TYPEABLE0(Z,zTC ,"Z") -- INSTANCE_TYPEABLE1(S,sTC ,"S")

@@ -5,6 +5,7 @@            , ScopedTypeVariables, CPP            , RankNTypes            , MultiParamTypeClasses, FunctionalDependencies+           , DeriveDataTypeable   #-} {-# OPTIONS_GHC -Wall #-} @@ -44,13 +45,11 @@  import Prelude hiding (foldr,sum,and) --- #include "Typeable.h"- import Data.Monoid (Monoid(..)) import Control.Applicative (Applicative(..),liftA2,(<$>)) import Data.Foldable (Foldable(..),toList,sum) -- ,and import Data.Traversable (Traversable(..))--- import Data.Typeable+import Data.Typeable (Typeable)  import Foreign.Storable import Foreign.Ptr (Ptr,plusPtr,castPtr)@@ -70,6 +69,7 @@ data Vec :: * -> * -> * where   ZVec :: Vec Z a    (:<) :: a -> Vec n a -> Vec (S n) a+ deriving Typeable  -- | Type-safe un-cons for vectors unConsV :: Vec (S n) a -> (a, Vec n a)@@ -516,6 +516,11 @@ --     from the context (n ~ S n1)  -}++-- resplit :: (Vec m a, Vec n a) -> (Vec n a, Vec m a)+-- resplit (u,v) = split (u <+> v)+-- +-- Won't type-check without commutativity of addition. :(  {- 

@@ -1,5 +1,5 @@ Name:                type-unary-Version:             0.2.8+Version:             0.2.13 Cabal-Version:       >= 1.6 Synopsis:               Type-level and typed unary natural numbers, inequality proofs, vectors@@ -11,7 +11,7 @@ Author:              Conal Elliott Maintainer:          conal@conal.net Homepage:            https://github.com/conal/type-unary-Copyright:           (c) 2009-2012 by Conal Elliott+Copyright:           (c) 2009-2014 by Conal Elliott License:             BSD3 License-File:        COPYING Stability:           provisional@@ -25,7 +25,7 @@ Library   hs-Source-Dirs:      src   Extensions:-  Build-Depends:       base >=4 && < 5, ty, vector-space, applicative-numbers+  Build-Depends:       base >=4 && < 5, ty>=0.1.5, vector-space, applicative-numbers   Exposed-Modules:                             TypeUnary.TyNat                        TypeUnary.Nat@@ -33,3 +33,4 @@                           ghc-options:         -Wall + ghc-prof-options:    -prof -auto-all