TypeNat (empty) → 0.1.0.0

raw patch · 6 files changed

+218/−0 lines, 6 filesdep +basesetup-changed

Dependencies added: base

Files

Data/TypeNat/Fin.hs +48/−0
Data/TypeNat/Nat.hs +46/−0
Data/TypeNat/Vect.hs +78/−0
LICENSE +20/−0
Setup.hs +2/−0
TypeNat.cabal +24/−0

+ Data/TypeNat/Fin.hs view

@@ -0,0 +1,48 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE GADTs #-}++module Data.TypeNat.Fin (++    Fin(..)++  , ix1+  , ix2+  , ix3+  , ix4+  , ix5+  , ix6+  , ix7+  , ix8+  , ix9+  , ix10++  , safeIndex++  , module Data.TypeNat.Nat++  ) where++import Data.TypeNat.Nat+import Data.TypeNat.Vect++-- | Finite set datatype.+data Fin :: Nat -> * where+  FZ :: Fin (S n)+  FS :: Fin k -> Fin (S k)++ix1 = FZ+ix2 = FS ix1+ix3 = FS ix2+ix4 = FS ix3+ix5 = FS ix4+ix6 = FS ix5+ix7 = FS ix6+ix8 = FS ix7+ix9 = FS ix8+ix10 = FS ix9++-- | Safely index a Vect.+safeIndex :: Vect a n -> Fin n -> a+safeIndex (VCons a _) FZ = a+safeIndex (VCons _ v) (FS x) = safeIndex v x

+ Data/TypeNat/Nat.hs view

@@ -0,0 +1,46 @@+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE Rank2Types #-}++module Data.TypeNat.Nat (++    Nat(..)+  , IsNat+  , natRecursion++  , One+  , Two+  , Three+  , Four+  , Five+  , Six+  , Seven+  , Eight+  , Nine+  , Ten++  ) where++data Nat = Z | S Nat++type One = S Z+type Two = S One+type Three = S Two+type Four = S Three+type Five = S Four+type Six = S Five+type Seven = S Six+type Eight = S Seven+type Nine = S Eight+type Ten = S Nine++-- | Proof that a given type is a Nat.+--   With this fact, you can do type-directed computation.+class IsNat (n :: Nat) where+  natRecursion :: (forall m . b -> a m -> a (S m)) -> (b -> a Z) -> (b -> b) -> b -> a n++instance IsNat Z where+  natRecursion _ ifZ _ = ifZ++instance IsNat n => IsNat (S n) where+  natRecursion ifS ifZ reduce x = ifS x (natRecursion ifS ifZ reduce (reduce x))

+ Data/TypeNat/Vect.hs view

@@ -0,0 +1,78 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE GADTs #-}++module Data.TypeNat.Vect (++    Vect(..)++  , vectMap+  , vectSnoc+  , vectToList+  , listToVect+  , showVect++  , module Data.TypeNat.Nat++  ) where++import Data.TypeNat.Nat++-- | Nat-indexed list, where the nat determines the length.+data Vect :: * -> Nat -> * where+  VNil :: Vect a Z+  VCons :: a -> Vect a n -> Vect a (S n)++-- | A kind of fmap for Vect.+vectMap :: (a -> b) -> Vect a n -> Vect b n+vectMap f vect = case vect of+  VNil -> VNil+  VCons x v -> VCons (f x) (vectMap f v)++-- | VCons to the end of a Vect.+vectSnoc :: a -> Vect a n -> Vect a (S n)+vectSnoc x vect = case vect of+  VNil -> VCons x VNil+  VCons y v -> VCons y (vectSnoc x v)++showVect :: Show a => Vect a l -> String+showVect VNil = "VNil"+showVect (VCons x xs) = show x ++ " , " ++ showVect xs++-- | Drop the length index from a Vect, giving a typical list.+vectToList :: Vect a n -> [a]+vectToList v = case v of+  VNil -> []+  VCons x xs -> x : vectToList xs++-- | Used to implement listToVect through natRecursion.+newtype MaybeVect a n = MV {+    unMV :: Maybe (Vect a n)+  }++-- | Try to produce a Vect from a list. The nat index must be fixed somehow,+--   perhaps with the help of ScopedTypeVariables.+listToVect:: IsNat n => [a] -> Maybe (Vect a n)+listToVect = unMV . listToVect'++  where++    listToVect':: IsNat n => [a] -> MaybeVect a n+    listToVect' = natRecursion inductive base reduce+    +    inductive :: [a] -> MaybeVect a m -> MaybeVect a (S m)+    inductive xs maybeVect = case maybeVect of+      MV Nothing -> MV Nothing+      MV (Just vect) -> case xs of +        [] -> MV Nothing+        (x : _) -> MV (Just (VCons x vect))++    base :: [a] -> MaybeVect a Z+    base xs = case xs of+      [] -> MV (Just VNil)+      _ -> MV Nothing++    reduce :: [a] -> [a]+    reduce xs = case xs of+      [] -> []+      (x : xs) -> xs

+ LICENSE view

@@ -0,0 +1,20 @@+Copyright (c) 2015 Alexander Vieth++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ TypeNat.cabal view

@@ -0,0 +1,24 @@+-- Initial TypeNat.cabal generated by cabal init.  For further +-- documentation, see http://haskell.org/cabal/users-guide/++name:                TypeNat+version:             0.1.0.0+synopsis:            Some Nat-indexed types for GHC+-- description:         +homepage:            https://github.com/avieth/TypeNat+license:             MIT+license-file:        LICENSE+author:              Alexander Vieth+maintainer:          aovieth@gmail.com+-- copyright:           +category:            Data+build-type:          Simple+cabal-version:       >=1.10++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+  -- hs-source-dirs:      +  default-language:    Haskell2010