type-unary 0.2.1 → 0.2.2
raw patch · 4 files changed
+220/−17 lines, 4 filesdep ~base
Dependency ranges changed: base
Files
- src/TypeUnary/Nat.hs +113/−4
- src/TypeUnary/TyNat.hs +8/−1
- src/TypeUnary/Vec.hs +98/−11
- type-unary.cabal +1/−1
src/TypeUnary/Nat.hs view
@@ -1,5 +1,6 @@ {-# LANGUAGE TypeOperators, GADTs, KindSignatures, RankNTypes #-} {-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -Wall #-} ---------------------------------------------------------------------- -- |@@ -21,8 +22,10 @@ , withIsNat, natSucc, natIsNat , natToZ, natEq, natAdd, natMul , IsNat(..)+ , induction -- * Inequality proofs and indices- , (:<:)(..), Index(..), unIndex, succI, index0, index1, index2, index3+ , (:<:)(..), succLim+ , Index(..), unIndex, succI, index0, index1, index2, index3 , coerceToIndex ) where @@ -113,6 +116,23 @@ -- and zero, ..., four, considering that all of them can be synthesized -- from IsNat. +-- | Peano's induction principle+induction :: forall p. + p Z -> (forall n. IsNat n => p n -> p (S n))+ -> (forall n. IsNat n => p n)+induction z s = go nat+ where+ -- morphism over z & s.+ go :: forall n. Nat n -> p n+ go Zero = z+ go (Succ m) = s (go m)++-- TODO: Use induction for n + Z == n. Then associativity and commutativity.++{--------------------------------------------------------------------+ Inequality proofs+--------------------------------------------------------------------}+ infix 4 :<: -- | Proof that @m < n@@@ -120,6 +140,77 @@ ZLess :: Z :<: S n SLess :: m :<: n -> S m :<: S n +-- | Increase the upper limit in an inequality proof+succLim :: m :<: n -> m :<: S n+succLim ZLess = ZLess+succLim (SLess p) = SLess (succLim p)++-- Note: succLim is a morphism++-- addLim :: forall p m n. IsNat p => +-- m :<: n -> m :<: (p :+: n)+-- addLim = addLim' nat++-- addLim' :: Nat p -> m :<: n -> m :<: (p :+: n)+-- addLim' Zero mn = mn+-- addLim' (Succ p') mn = bump p' (addLim' p' mn)+++-- addLim mn = case (nat :: Nat p) of+-- Zero -> mn+-- -- Succ p' -> bump p' (addLim mn)+-- -- Succ (p' :: Nat p') -> bump p' (addLim mn :: (m :<: p' :+: n))+-- Succ (p' :: Nat p') -> undefined p' (addLim mn :: (m :<: p' :+: n))++-- p :: S p'++-- S p' + n = S (p' + n)++-- Succ (p' :: Nat p') -> succLim (addLim mn :: (m :<: p' :+: n))++-- bump :: Nat p+-- -> (m :<: (p :+: n))+-- -> (m :<: S (p :+: n))+-- bump = undefined++-- addLim = case (nat :: Nat p) of+-- Zero -> id+-- Succ p' -> succLim . addLim++-- p :: S p'+-- p = Succ p'++-- p + n == S (p' + n)++-- mn :: m < n+-- addLim mn :: m < p' + n+-- succLim (addLim mn) :: m < S (p' + n)+++-- mn :: S m :<: S n+-- mn = SLess mn'+-- mn' :: m :<: n+++++-- Z + n == n++-- S p' + n == S (p' + n)++-- mn :: S m < S n+-- mn' :: m < n++-- p :: S p'+-- p' :: p'++-- ... :: S m :<: (S p' :+: n)+-- ... :: S m :<: S (p' :+: S n)++-- addLim' :: forall p m n. IsNat p => +-- Nat p -> m :<: n -> m :<: (p :+: n)+-- addLim' Zero = id+ -- | A number under the given limit, with proof data Index lim = forall n. IsNat n => Index (n :<: lim) (Nat n) @@ -154,18 +245,36 @@ -- | Index generation from integer. Can fail dynamically if the integer is -- too large.-coerceToIndex :: (Show i, Integral i, IsNat m) => i -> Index m+coerceToIndex :: (Show i, Num i, IsNat m) => i -> Index m coerceToIndex = coerceToIndex' nat -coerceToIndex' :: (Show i, Integral i) => Nat m -> i -> Index m+coerceToIndex' :: (Show i, Num i) => Nat m -> i -> Index m coerceToIndex' mOrig niOrig = loop mOrig niOrig where- loop :: (Show i, Integral i) => Nat m -> i -> Index m+ loop :: (Show i, Num i) => Nat m -> i -> Index m loop Zero _ = error $ "coerceToIndex: out of bounds: " ++ show niOrig ++ " should be less than " ++ show mOrig loop (Succ _) 0 = Index ZLess Zero loop (Succ m') ni' = succI (loop m' (ni'-1))++-- Experimental instances:++instance Show (Index n) where+ show (Index _ n) = show n++instance IsNat n => Num (Index n) where+ fromInteger = coerceToIndex+ (+) = noIndex "(+)"+ (*) = noIndex "(*)"+ abs = noIndex "abs"+ signum = noIndex "signum"++noIndex :: String -> a+noIndex meth = error (meth ++ ": no method for Index n. Sorry.")++-- TODO: Perhaps replace these noIndex uses with real definitions. However, it+-- doesn't seem likely that we'd want to stay in Index n for the same n. {-------------------------------------------------------------------- IsNat
src/TypeUnary/TyNat.hs view
@@ -16,7 +16,7 @@ module TypeUnary.TyNat ( -- * Type-level natural numbers- Z, S, (:+:), (:*:)+ Z, S, (:+:), (:*:), (:-:) , N0,N1,N2,N3,N4,N5,N6,N7,N8,N9,N10,N11,N12,N13,N14,N15,N16 ) where @@ -45,6 +45,13 @@ type instance Z :*: b = Z type instance S a :*: b = b :+: (a :*: b) +infixl 6 :-:++-- Experiment:+type family a :-: b++type instance n :-: Z = n+type instance S n :-: S m = n :-: m -- Generated code --
src/TypeUnary/Vec.hs view
@@ -32,19 +32,21 @@ , update , set, set0, set1, set2, set3 , getI, setI- , flattenV, swizzle, split, deleteV, elemsV, unzipV+ , flattenV, swizzle, split, deleteV, elemsV+ , zipV , zipWithV , unzipV+ , zipV3, zipWithV3, unzipV3 , ToVec(..) ) where -- TODO: Consider dropping "V" suffix from several of the names. -import Prelude hiding (foldr,sum)+import Prelude hiding (foldr,sum,and) -- #include "Typeable.h" import Data.Monoid (Monoid(..)) import Control.Applicative (Applicative(..),liftA2,(<$>))-import Data.Foldable (Foldable(..),toList,sum)+import Data.Foldable (Foldable(..),toList,sum) -- ,and import Data.Traversable (Traversable(..)) -- import Data.Typeable @@ -113,11 +115,27 @@ instance Ord a => Ord (Vec n a) where ZVec `compare` ZVec = EQ (a :< as) `compare` (b :< bs) =- case a `compare` b of- LT -> LT- GT -> GT- EQ -> as `compare` bs+ (a `compare` b) `mappend` (as `compare` bs) +-- Equivalently,+-- +-- (a :< as) `compare` (b :< bs) =+-- case a `compare` b of+-- LT -> LT+-- GT -> GT+-- EQ -> as `compare` bs++-- Some alternatives:+-- +-- (==*) :: (IsNat n, Eq a) => Vec n a -> Vec n a -> Bool+-- (==*) = (fmap.fmap) and (liftA2 (==))+-- +-- -- as ==* bs = and (liftA2 (==) as bs)+-- +-- compare' :: (IsNat n, Ord a) => Vec n a -> Vec n a -> Ordering+-- compare' = (fmap.fmap) fold (liftA2 compare)++ instance Show a => Show (Vec n a) where show v = "elemsV " ++ show (toList v) @@ -320,7 +338,7 @@ -- TODO: consider this notation: ----- infixr 5 :<+-- infixr 5 <| -- (<|) :: a -> a -> Vec2 a -- (<|) = vec2 -- @@ -391,9 +409,13 @@ -- | Swizzling. Extract multiple elements simultaneously. swizzle :: Vec n (Index m) -> Vec m a -> Vec n a-swizzle ZVec _ = ZVec-swizzle (ix :< ixs) v = get ix v :< swizzle ixs v+swizzle is v = flip get v <$> is +-- swizzle ZVec _ = ZVec+-- swizzle (ix :< ixs) v = get ix v :< swizzle ixs v++-- swizzle = flip (fmap . flip get)+ -- | Split a vector split :: IsNat n => Vec (n :+: m) a -> (Vec n a, Vec m a) split = split' nat@@ -425,8 +447,44 @@ -- at /Users/conal/Haskell/type-unary/src/TypeUnary/Vec.hs:488:1-18 -- NB: `:+:' is a type function, and may not be injective ++-- Alternatively:+ {-+take :: forall m n a. (IsNat n, IsNat m) => Vec (n :+: m) a -> Vec n a+take = take' (nat :: Nat n) (nat :: Nat m) +take' :: Nat n -> Nat m -> Vec (n :+: m) a -> Vec n a+take' Zero _ _ = ZVec+take' (Succ n) m (a :< as) = a :< take' n m as+-}++-- I think it'd be hard to use take. I guess we'd have to subtract in the type+-- system.++{-++take :: forall m n a. (IsNat n, IsNat m) =>+ Vec (n :+: m) a -> (Vec n a,Nat m)+take = take' (nat :: Nat n)++take' :: Nat n -> Vec (n :+: m) a -> (Vec n a,Nat m)+take' Zero as = (ZVec,lengthV as)+take' (Succ n) (a :< as) = (a :< as', m)+ where+ (as',m) = take' n as++lengthV :: Vec n a -> Nat n+lengthV ZVec = Zero+lengthV (a :< as) = Succ (lengthV as)++-- Could not deduce (IsNat n1) arising from a use of `Succ'+-- from the context (n ~ S n1)++-}++{-+ -- Reversal. Thinking about this one. Currently thwarted by missing -- knowledge about numbers in the type-checker. Would be easy with -- built-in type-level naturals.@@ -477,10 +535,39 @@ t3 = swizzle t2 t1 -} --- | Unzip a list of pairs into a pair of lists+-- | Zip two vectors into one. Like @'liftA2' '(,)'@, but the former requires+-- @IsNat n@.+zipV :: Vec n a -> Vec n b -> Vec n (a,b)+zipV = zipWithV (,)++-- | Zip three vectors into one. Like @'liftA3' '(,)'@, but the former requires+-- @IsNat n@.+zipV3 :: Vec n a -> Vec n b -> Vec n c -> Vec n (a,b,c)+zipV3 = zipWithV3 (,,)++-- | Unzip one vector into two. Like 'liftA2', but the former requires+-- @IsNat n@.+zipWithV :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c+zipWithV _ ZVec ZVec = ZVec+zipWithV f (a :< as) (b :< bs) = f a b :< zipWithV f as bs++-- | Unzip one vector into two. Like 'liftA2', but the former requires+-- @IsNat n@.+zipWithV3 :: (a -> b -> c -> d) -> Vec n a -> Vec n b -> Vec n c -> Vec n d+zipWithV3 _ ZVec ZVec ZVec = ZVec+zipWithV3 f (a :< as) (b :< bs) (c :< cs) = f a b c :< zipWithV3 f as bs cs++-- | Unzip a vector of pairs into a pair of vectors unzipV :: Vec n (a,b) -> (Vec n a, Vec n b) unzipV ZVec = (ZVec,ZVec) unzipV ((a,b) :< ps) = (a :< as, b :< bs) where (as,bs) = unzipV ps++-- | Unzip a vector of pairs into a pair of vectors+unzipV3 :: Vec n (a,b,c) -> (Vec n a, Vec n b, Vec n c)+unzipV3 ZVec = (ZVec,ZVec,ZVec)+unzipV3 ((a,b,c) :< ps) = (a :< as, b :< bs, c :< cs) + where (as,bs,cs) = unzipV3 ps+ {-------------------------------------------------------------------- Conversion to vectors
type-unary.cabal view
@@ -1,5 +1,5 @@ Name: type-unary-Version: 0.2.1+Version: 0.2.2 Cabal-Version: >= 1.2 Synopsis: Type-level and typed unary natural numbers, inequality proofs, vectors