natural-number (empty) → 1.0

raw patch · 4 files changed

+117/−0 lines, 4 filesdep +basedep +type-equalitydep +type-level-natural-numbersetup-changed

Dependencies added: base, type-equality, type-level-natural-number, type-level-natural-number-induction

Files

• Data/NaturalNumber.hs +70/−0
• LICENSE +22/−0
• Setup.hs +2/−0
• natural-number.cabal +23/−0

@@ -0,0 +1,70 @@+{-# LANGUAGE GADTs #-}++module Data.NaturalNumber where++import Data.Typeable+import Data.Type.Equality++import TypeLevel.NaturalNumber hiding (NaturalNumber)+import qualified TypeLevel.NaturalNumber as TLN+import TypeLevel.NaturalNumber.Induction++data N a where+    NZero :: N Zero+    NSuccessorTo :: N n -> N (SuccessorTo n)++data UnknownN where+    UnknownN :: NaturalNumber n => N n -> UnknownN++class (TLN.NaturalNumber n, Induction n) => NaturalNumber n where+    asN :: N n+    fromN :: N n -> n+instance NaturalNumber Zero where+    asN = NZero+    fromN _ = undefined+instance NaturalNumber n => NaturalNumber (SuccessorTo n) where+    asN = NSuccessorTo asN+    fromN _ = undefined++instance NaturalNumber n => Typeable (N n) where+    typeOf n = mkTyConApp (mkTyCon $ "N#" ++ (show . naturalNumberAsInt . fromN) n) []++instance Show (N n) where+    show = show . nToInt++instance Show UnknownN where+    show (UnknownN n) = show n++instance Eq (N n) where+    (==) _ _ = True+    (/=) _ _ = False++instance EqT N where+    eqT NZero NZero = Just Refl+    eqT (NSuccessorTo m) (NSuccessorTo n) =+        case m `eqT` n of+             Just Refl -> Just Refl+             Nothing -> Nothing+    eqT _ _ = Nothing++nToInt :: N n -> Int+nToInt NZero = 0+nToInt (NSuccessorTo n) = 1 + nToInt n++unknownNToInt :: UnknownN -> Int+unknownNToInt (UnknownN n) = nToInt n++intToUnknownN :: Int -> UnknownN+intToUnknownN i+  | i < 0 = error $ "Cannot convert negative number " ++ show i ++ " to a natural number."+  | otherwise = go i+  where+    go 0 = UnknownN NZero+    go i = case go (i-1) of UnknownN n -> UnknownN (NSuccessorTo n)++intToN :: NaturalNumber n => Int -> N n+intToN i+  | i == nToInt n = n+  | otherwise = error $ show i ++ " /= " ++ show n+  where n = asN+

@@ -0,0 +1,22 @@+Copyright (c) 2010, Gregory M. Crosswhite+All rights reserved.++Redistribution and use in source and binary forms, with or without modification,+are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright notice,+      this list of conditions and the following disclaimer.+    * Redistributions in binary form must reproduce the above copyright notice,+      this list of conditions and the following disclaimer in the documentation+      and/or other materials provided with the distribution.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

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

@@ -0,0 +1,23 @@+Name:                natural-number+Version:             1.0+License:             BSD3+License-file:        LICENSE+Author:              Gregory Crosswhite+Maintainer:          Gregory Crosswhite <gcross@phys.washington.edu>+Stability:           Provisional+Synopsis:            Natural numbers tagged with a type-level representation of the number.+Description:         This package provides a simple data structure for+                     repesenting natural numbers with a type that is tagged+     	             with the type-level natural number corresponding to the+                     value of the natural number.+Cabal-version:       >=1.2.3+Build-type:          Simple+Category:	     Type System,Data++Library+    Build-depends:   base >= 3 && < 5,+                     type-level-natural-number >= 1.0 && < 1.2,+                     type-level-natural-number-induction >= 1.0 && < 1.1,+                     type-equality >= 0.1 && < 0.2+    Exposed-modules: Data.NaturalNumber+    Extensions:	     GADTs