packages feed

fin (empty) → 0

raw patch · 9 files changed

+1286/−0 lines, 9 filesdep +basedep +deepseqdep +finsetup-changed

Dependencies added: base, deepseq, fin, hashable, inspection-testing, nats, semigroups, tagged, void

Files

+ ChangeLog.md view
@@ -0,0 +1,4 @@+# Revision history for boring+## 0++- First version. Released on an unsuspecting world.
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2017, Oleg Grenrus++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.++    * Neither the name of Oleg Grenrus nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ fin.cabal view
@@ -0,0 +1,104 @@+name:                fin+version:             0+synopsis:            Nat and Fin+description:+  This package provides two simple types, and some tools to work with them.+  Also on type level as @DataKinds@.+  .+  @+  data Nat = Z | S Nat+  data Fin (n :: Nat) where+    Z :: Fin n+    S :: Fin n -> Fin ('Nat.S n)+  @+  .+  The "Data.Fin.Enum" module let's work generically with enumerations.+  .+  Differences to other packages:+  .+  * [type-natural](http://hackage.haskell.org/package/type-natural) depends+    on @singletons@ package. `fin` will try to stay light on the dependencies,+    and support as many GHC versions as practical.+  .+  * [peano](http://hackage.haskell.org/package/peano) is very incomplete+  .+  * [nat](http://hackage.haskell.org/package/nat) as well.+  .+  * [PeanoWitnesses](https://hackage.haskell.org/package/PeanoWitnesses)+    doesn't use @DataKinds@.+  .+  * [type-combinators](http://hackage.haskell.org/package/type-combinators)+    is big package too.+homepage:            https://github.com/phadej/vec+bug-reports:         https://github.com/phadej/vec/issues+license:             BSD3+license-file:        LICENSE+author:              Oleg Grenrus <oleg.grenrus@iki.fi>+maintainer:          Oleg.Grenrus <oleg.grenrus@iki.fi>+copyright:           (c) 2017 Oleg Grenrus+category:            Data+build-type:          Simple+extra-source-files:  ChangeLog.md+cabal-version:       >=1.10+tested-with:+  GHC==7.8.4,+  GHC==7.10.3,+  GHC==8.0.2,+  GHC==8.2.1++source-repository head+  type:      git+  location:  https://github.com/phadej/vec.git++library+  exposed-modules:+    Data.Fin+    Data.Fin.Enum+    Data.Nat+    Data.Type.Nat+  build-depends:+    base     >=4.7     && <4.11,+    deepseq  >=1.3.0.2 && <1.5,+    hashable >=1.2.6.1 && <1.3++  if !impl(ghc >= 8.0)+    build-depends:+      semigroups >=0.18.3 && <0.18.4++  if !impl(ghc >= 7.10)+    build-depends:+       nats >=1     && <1.2,+       void >=0.7.2 && <0.8++  ghc-options:         -Wall -fprint-explicit-kinds+  hs-source-dirs:      src+  default-language:    Haskell2010++  -- dump-core+  -- if impl(ghc >= 8.0)+  --  build-depends: dump-core+  --  ghc-options: -fplugin=DumpCore -fplugin-opt DumpCore:core-html++test-suite inspection+  type:                exitcode-stdio-1.0+  main-is:             Inspection.hs+  ghc-options:         -Wall -fprint-explicit-kinds+  hs-source-dirs:      test+  default-language:    Haskell2010+  build-depends:+    base,+    fin,+    tagged,+    inspection-testing >= 0.1.2 && <0.2++  if !impl(ghc >= 8.0)+    buildable: False++  -- useful for development+  ghc-options:+  -- -dsuppress-idinfo+  -- -dsuppress-coercions+  -- -dsuppress-type-applications+  -- -dsuppress-module-prefixes+  -- -dsuppress-type-signatures+  -- -dsuppress-uniques
+ src/Data/Fin.hs view
@@ -0,0 +1,311 @@+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE DeriveDataTypeable   #-}+{-# LANGUAGE EmptyCase            #-}+{-# LANGUAGE GADTs                #-}+{-# LANGUAGE KindSignatures       #-}+{-# LANGUAGE ScopedTypeVariables  #-}+{-# LANGUAGE StandaloneDeriving   #-}+{-# LANGUAGE UndecidableInstances #-}+-- | Finite numbers.+--+-- This module is designed to be imported qualified.+module Data.Fin (+    Fin (..),+    cata,+    -- * Showing+    explicitShow,+    explicitShowsPrec,+    -- * Conversions+    toNat,+    fromNat,+    toNatural,+    toInteger,+    -- * Interesting+    inverse,+    universe,+    inlineUniverse,+    universe1,+    inlineUniverse1,+    absurd,+    boring,+    -- * Aliases+    fin0, fin1, fin2, fin3, fin4, fin5, fin6, fin7, fin8, fin9,+    ) where++import Control.DeepSeq    (NFData (..))+import Data.Hashable      (Hashable (..))+import Data.List.NonEmpty (NonEmpty (..))+import Data.Proxy         (Proxy (..))+import Data.Typeable      (Typeable)+import GHC.Exception      (ArithException (..), throw)+import Numeric.Natural    (Natural)++import qualified Data.List.NonEmpty as NE+import qualified Data.Type.Nat      as N++-- | Finite Numbers up to 'n'.+data Fin (n :: N.Nat) where+    Z :: Fin ('N.S n)+    S :: Fin n -> Fin ('N.S n)+  deriving (Typeable)++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++deriving instance Eq (Fin n)+deriving instance Ord (Fin n)++-- | 'Fin' is printed as 'Natural'.+--+-- To see explicit structure, use 'explicitShow' or 'explicitShowsPrec'+instance Show (Fin n) where+    showsPrec d  = showsPrec d . toNatural++-- | Operations module @n@.+--+-- >>> map fromInteger [0, 1, 2, 3, 4, -5] :: [Fin N.Nat3]+-- [0,1,2,0,1,1]+--+-- >>> fromInteger 42 :: Fin N.Nat0+-- *** Exception: divide by zero+-- ...+--+-- >>> signum (Z :: Fin N.Nat1)+-- 0+--+-- >>> signum (3 :: Fin N.Nat4)+-- 1+--+-- >>> 2 + 3 :: Fin N.Nat4+-- 1+--+-- >>> 2 * 3 :: Fin N.Nat4+-- 2+--+instance N.SNatI n => Num (Fin n) where+    abs = id++    signum Z         = Z+    signum (S Z)     = S Z+    signum (S (S _)) = S Z++    fromInteger = unsafeFromNum . (`mod` (N.reflectToNum (Proxy :: Proxy n)))++    n + m = fromInteger (toInteger n + toInteger m)+    n * m = fromInteger (toInteger n * toInteger m)+    n - m = fromInteger (toInteger n - toInteger m)++    negate = fromInteger . negate . toInteger++instance N.SNatI n => Real (Fin n) where+    toRational = cata 0 succ++-- | 'quot' works only on @'Fin' n@ where @n@ is prime.+instance N.SNatI n => Integral (Fin n) where+    toInteger = cata 0 succ++    quotRem a b = (quot a b, 0)+    quot a b = a * inverse b++-- | Multiplicative inverse.+--+-- Works for @'Fin' n@ where @n@ is coprime with an argument, i.e. in general when @n@ is prime.+--+-- >>> map inverse universe :: [Fin N.Nat5]+-- [0,1,3,2,4]+--+-- >>> zipWith (*) universe (map inverse universe) :: [Fin N.Nat5]+-- [0,1,1,1,1]+--+-- Adaptation of [pseudo-code in Wikipedia](https://en.wikipedia.org/wiki/Extended_Euclidean_algorithm#Modular_integers)+--+inverse :: forall n. N.SNatI n => Fin n -> Fin n+inverse = fromInteger . iter 0 n 1 . toInteger where+    n = N.reflectToNum (Proxy :: Proxy n)++    iter t _ _  0+        | t < 0     = t + n+        | otherwise = t+    iter t r t' r' =+        let q = r `div` r'+        in iter t' r' (t - q * t') (r - q * r')++instance N.SNatI n => Enum (Fin n) where+    fromEnum = go where+        go :: Fin m -> Int+        go Z     = 0+        go (S n) = succ (go n)++    toEnum = unsafeFromNum++instance (n ~ 'N.S m, N.SNatI m) => Bounded (Fin n) where+    minBound = Z+    maxBound = getMaxBound $ N.induction+        (MaxBound Z)+        (MaxBound . S . getMaxBound)++newtype MaxBound n = MaxBound { getMaxBound :: Fin ('N.S n) }++instance NFData (Fin n) where+    rnf Z     = ()+    rnf (S n) = rnf n++instance Hashable (Fin n) where+    hashWithSalt salt = hashWithSalt salt . cata (0 :: Integer) succ++-------------------------------------------------------------------------------+-- Showing+-------------------------------------------------------------------------------++-- | 'show' displaying a structure of 'Fin'.+--+-- >>> explicitShow (0 :: Fin N.Nat1)+-- "Z"+--+-- >>> explicitShow (2 :: Fin N.Nat3)+-- "S (S Z)"+--+explicitShow :: Fin n -> String+explicitShow n = explicitShowsPrec 0 n ""++-- | 'showsPrec' displaying a structure of 'Fin'.+explicitShowsPrec :: Int -> Fin n -> ShowS+explicitShowsPrec _ Z     = showString "Z"+explicitShowsPrec d (S n) = showParen (d > 10)+    $ showString "S "+    . explicitShowsPrec 11 n++-------------------------------------------------------------------------------+-- Conversions+-------------------------------------------------------------------------------++-- | Fold 'Fin'.+cata :: forall a n. a -> (a -> a) -> Fin n -> a+cata z f = go where+    go :: Fin m -> a+    go Z = z+    go (S n) = f (go n)++-- | Convert to 'Nat'.+toNat :: Fin n -> N.Nat+toNat = cata N.Z N.S++-- | Convert from 'Nat'.+--+-- >>> fromNat N.nat1 :: Maybe (Fin N.Nat2)+-- Just 1+--+-- >>> fromNat N.nat1 :: Maybe (Fin N.Nat1)+-- Nothing+--+fromNat :: N.SNatI n => N.Nat -> Maybe (Fin n)+fromNat = appNatToFin (N.induction start step) where+    start :: NatToFin 'N.Z+    start = NatToFin $ const Nothing++    step :: NatToFin n -> NatToFin ('N.S n)+    step (NatToFin f) = NatToFin $ \n -> case n of+        N.Z   -> Just Z+        N.S m -> fmap S (f m)++newtype NatToFin n = NatToFin { appNatToFin :: N.Nat -> Maybe (Fin n) }++-- | Convert to 'Natural'.+toNatural :: Fin n -> Natural+toNatural = cata 0 succ++-- | Convert from any 'Ord' 'Num'.+unsafeFromNum :: forall n i. (Num i, Ord i, N.SNatI n) => i -> Fin n+unsafeFromNum = appUnsafeFromNum (N.induction start step) where+    start :: UnsafeFromNum i 'N.Z+    start = UnsafeFromNum $ \n -> case compare n 0 of+        LT -> throw Underflow+        EQ -> throw Overflow+        GT -> throw Overflow++    step :: UnsafeFromNum i m -> UnsafeFromNum i ('N.S m)+    step (UnsafeFromNum f) = UnsafeFromNum $ \n -> case compare n 0 of+        EQ -> Z+        GT -> S (f (n - 1))+        LT -> throw Underflow++newtype UnsafeFromNum i n = UnsafeFromNum { appUnsafeFromNum :: i -> Fin n }++-------------------------------------------------------------------------------+-- "Interesting" stuff+-------------------------------------------------------------------------------++-- | All values. @[minBound .. maxBound]@ won't work for @'Fin' 'N.Nat0'@.+--+-- >>> universe :: [Fin N.Nat3]+-- [0,1,2]+universe :: N.SNatI n => [Fin n]+universe = getUniverse $ N.induction (Universe []) step where+    step :: Universe n -> Universe ('N.S n)+    step (Universe xs) = Universe (Z : map S xs)++-- | Like 'universe' but 'NonEmpty'.+--+-- >>> universe1 :: NonEmpty (Fin N.Nat3)+-- 0 :| [1,2]+universe1 :: N.SNatI n => NonEmpty (Fin ('N.S n))+universe1 = getUniverse1 $ N.induction (Universe1 (Z :| [])) step where+    step :: Universe1 n -> Universe1 ('N.S n)+    step (Universe1 xs) = Universe1 (NE.cons Z (fmap S xs))++-- | 'universe' which will be fully inlined, if @n@ is known at compile time.+--+-- >>> inlineUniverse :: [Fin N.Nat3]+-- [0,1,2]+inlineUniverse :: N.InlineInduction n => [Fin n]+inlineUniverse = getUniverse $ N.inlineInduction (Universe []) step where+    step :: Universe n -> Universe ('N.S n)+    step (Universe xs) = Universe (Z : map S xs)++-- | >>> inlineUniverse1 :: NonEmpty (Fin N.Nat3)+-- 0 :| [1,2]+inlineUniverse1 :: N.InlineInduction n => NonEmpty (Fin ('N.S n))+inlineUniverse1 = getUniverse1 $ N.inlineInduction (Universe1 (Z :| [])) step where+    step :: Universe1 n -> Universe1 ('N.S n)+    step (Universe1 xs) = Universe1 (NE.cons Z (fmap S xs))++newtype Universe  n = Universe  { getUniverse  :: [Fin n] }+newtype Universe1 n = Universe1 { getUniverse1 :: NonEmpty (Fin ('N.S n)) }++-- | @'Fin' 'N.Nat0'@ is inhabited.+absurd :: Fin N.Nat0 -> b+absurd n = case n of {}++-- | Counting to one is boring.+--+-- >>> boring+-- 0+boring :: Fin N.Nat1+boring = Z++-------------------------------------------------------------------------------+-- Aliases+-------------------------------------------------------------------------------++fin0 :: Fin (N.Plus N.Nat0 ('N.S n))+fin1 :: Fin (N.Plus N.Nat1 ('N.S n))+fin2 :: Fin (N.Plus N.Nat2 ('N.S n))+fin3 :: Fin (N.Plus N.Nat3 ('N.S n))+fin4 :: Fin (N.Plus N.Nat4 ('N.S n))+fin5 :: Fin (N.Plus N.Nat5 ('N.S n))+fin6 :: Fin (N.Plus N.Nat6 ('N.S n))+fin7 :: Fin (N.Plus N.Nat7 ('N.S n))+fin8 :: Fin (N.Plus N.Nat8 ('N.S n))+fin9 :: Fin (N.Plus N.Nat9 ('N.S n))++fin0 = Z+fin1 = S fin0+fin2 = S fin1+fin3 = S fin2+fin4 = S fin3+fin5 = S fin4+fin6 = S fin5+fin7 = S fin6+fin8 = S fin7+fin9 = S fin8
+ src/Data/Fin/Enum.hs view
@@ -0,0 +1,162 @@+{-# LANGUAGE ConstraintKinds        #-}+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE DefaultSignatures      #-}+{-# LANGUAGE FlexibleContexts       #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE PolyKinds              #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+-- |+--+-- This module is designed to be imported qualified:+--+-- @+-- import qualified Data.Fin.Enum as E+-- @+--+module Data.Fin.Enum (+    Enum (..),+    -- * Generic implementation+    gfrom, GFrom,+    gto, GTo,+    GEnumSize,+    ) where++import Prelude hiding (Enum (..))++import Data.Fin     (Fin)+import Data.Nat     (Nat)+import Data.Proxy   (Proxy (..))+import GHC.Generics ((:+:) (..), M1 (..), U1 (..), V1)++import qualified Data.Fin      as F+import qualified Data.Type.Nat as N+import qualified Data.Void     as V+import qualified GHC.Generics  as G++-- | Generic enumerations.+--+-- /Examples:/+--+-- >>> from ()+-- 0+--+-- >>> to 0 :: ()+-- ()+--+-- >>> to 0 :: Bool+-- False+--+-- >>> map to F.universe :: [Bool]+-- [False,True]+--+-- >>> map (to . (+1) . from) [LT, EQ, GT] :: [Ordering] -- Num Fin is modulo arithmetic+-- [EQ,GT,LT]+--+class Enum a where+    -- | The size of an enumeration.+    type EnumSize a :: Nat+    type EnumSize a = GEnumSize a++    -- | Converts a value to its index.+    from :: a -> Fin (EnumSize a)+    default from :: (G.Generic a, GFrom a, EnumSize a ~ GEnumSize a) => a -> Fin (EnumSize a)+    from = gfrom++    -- | Converts from index to the original value.+    to :: Fin (EnumSize a) -> a+    default to :: (G.Generic a, GTo a, EnumSize a ~ GEnumSize a) => Fin (EnumSize a) -> a+    to = gto++-- | 'Void' ~ 0+instance Enum V.Void where+    -- this should be written by hand to work with all @base@+    type EnumSize V.Void = N.Nat0+    from = V.absurd+    to   = F.absurd++-- | () ~ 1+instance Enum ()++-- | 'Bool' ~ 2+instance Enum Bool++-- | 'Ordering' ~ 3+instance Enum Ordering++-------------------------------------------------------------------------------+-- EnumSize+-------------------------------------------------------------------------------++-- | Compute the size from the type.+type GEnumSize a = EnumSizeRep (G.Rep a) N.Nat0++type family EnumSizeRep (a :: * -> *) (n :: Nat) :: Nat where+    EnumSizeRep (a :+: b )   n = EnumSizeRep a (EnumSizeRep b n)+    EnumSizeRep V1           n = n+    EnumSizeRep (M1 _d _c a) n = EnumSizeRep a n+    EnumSizeRep U1           n = 'N.S n+    -- No instance for K1 or :*:++-------------------------------------------------------------------------------+-- From+-------------------------------------------------------------------------------++-- | Generic version of 'from'.+gfrom :: (G.Generic a, GFrom a) => a -> Fin (GEnumSize a)+gfrom = \x -> gfromRep (G.from x) (error "gfrom: internal error" :: Fin N.Nat0)++-- | Constraint for the class that computes 'gfrom'.+type GFrom a = GFromRep (G.Rep a)++class GFromRep (a :: * -> *)  where+    gfromRep  :: a x     -> Fin n -> Fin (EnumSizeRep a n)+    gfromSkip :: Proxy a -> Fin n -> Fin (EnumSizeRep a n)++instance (GFromRep a, GFromRep b) => GFromRep (a :+: b) where+    gfromRep (L1 a) n = gfromRep a (gfromSkip (Proxy :: Proxy b) n)+    gfromRep (R1 b) n = gfromSkip (Proxy :: Proxy a) (gfromRep b n)++    gfromSkip _ n = gfromSkip (Proxy :: Proxy a) (gfromSkip (Proxy :: Proxy b) n)++instance GFromRep a => GFromRep (M1 d c a) where+    gfromRep (M1 a) n = gfromRep a n+    gfromSkip _     n = gfromSkip (Proxy :: Proxy a) n++instance GFromRep V1 where+    gfromRep  _ n = n+    gfromSkip _ n = n++instance GFromRep U1 where+    gfromRep U1 _ = F.Z+    gfromSkip _ n = F.S n++-------------------------------------------------------------------------------+-- To+-------------------------------------------------------------------------------++-- | Generic version of 'to'.+gto :: (G.Generic a, GTo a) => Fin (GEnumSize a) -> a+gto = \x -> G.to $ gtoRep x id $ F.absurd++-- | Constraint for the class that computes 'gto'.+type GTo a = GToRep (G.Rep a)++class GToRep (a :: * -> *) where+    gtoRep :: Fin (EnumSizeRep a n) -> (a x -> r) -> (Fin n -> r) -> r++instance (GToRep a, GToRep b) => GToRep (a :+: b) where+    gtoRep n s k = gtoRep n (s . L1) $ \r -> gtoRep r (s . R1) k++instance GToRep a => GToRep (M1 d c a) where+    gtoRep n s = gtoRep n (s . M1)++instance GToRep V1 where+    gtoRep n _ k = k n++instance GToRep U1 where+    gtoRep F.Z     s _ = s U1+    gtoRep (F.S n) _ k = k n
+ src/Data/Nat.hs view
@@ -0,0 +1,170 @@+{-# LANGUAGE DeriveDataTypeable #-}+-- | 'Nat' numbers.+--+-- This module is designed to be imported qualified.+--+module Data.Nat (+    -- * Natural, Nat numbers+    Nat(..),+    toNatural,+    fromNatural,+    cata,+    -- * Showing+    explicitShow,+    explicitShowsPrec,+    -- * Aliases+    nat0, nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9,+    ) where++import Control.DeepSeq (NFData (..))+import Data.Data       (Data)+import Data.Hashable   (Hashable (..))+import Data.Typeable   (Typeable)+import GHC.Exception   (ArithException (..), throw)+import Numeric.Natural (Natural)++-------------------------------------------------------------------------------+-- Nat+-------------------------------------------------------------------------------++-- | Nat natural numbers.+--+-- Better than GHC's built-in 'GHC.TypeLits.Nat' for some use cases.+--+data Nat = Z | S Nat deriving (Eq, Ord, Typeable, Data)++-- | 'Nat' is printed as 'Natural'.+--+-- To see explicit structure, use 'explicitShow' or 'explicitShowsPrec'+--+instance Show Nat where+    showsPrec d = showsPrec d . toNatural++instance Num Nat where+    fromInteger = fromNatural . fromInteger++    Z   + m = m+    S n + m = S (n + m)++    Z   * _ = Z+    S n * m = (n * m) + m++    abs = id++    signum Z     = Z+    signum (S _) = S Z++    negate _ = error "negate @Nat"++instance Real Nat where+    toRational = toRational . toInteger++instance Integral Nat where+    toInteger = cata 0 succ++    quotRem _ Z = throw DivideByZero+    quotRem _ _ = error "un-implemented"++{- TODO: make <= with witness+instance Ix Nat where+    range = _++    inRange = _+-}++instance Enum Nat where+    toEnum n+        | n < 0     = throw Underflow+        | otherwise = iterate S Z !! n++    fromEnum = cata 0 succ++    succ       = S+    pred Z     = throw Underflow+    pred (S n) = n++instance NFData Nat where+    rnf Z     = ()+    rnf (S n) = rnf n++instance Hashable Nat where+    hashWithSalt salt = hashWithSalt salt . toInteger++-------------------------------------------------------------------------------+-- Showing+-------------------------------------------------------------------------------++-- | 'show' displaying a structure of 'Nat'.+--+-- >>> explicitShow 0+-- "Z"+--+-- >>> explicitShow 2+-- "S (S Z)"+--+explicitShow :: Nat -> String+explicitShow n = explicitShowsPrec 0 n ""++-- | 'showsPrec' displaying a structure of 'Nat'.+explicitShowsPrec :: Int -> Nat -> ShowS+explicitShowsPrec _ Z     = showString "Z"+explicitShowsPrec d (S n) = showParen (d > 10)+    $ showString "S "+    . explicitShowsPrec 11 n++-------------------------------------------------------------------------------+-- Conversions+-------------------------------------------------------------------------------++-- | Fold 'Nat'.+--+-- >>> cata [] ('x' :) 2+-- "xx"+--+cata :: a -> (a -> a) -> Nat -> a+cata z f = go where+    go Z     = z+    go (S n) = f (go n)++-- | Convert 'Nat' to 'Natural'+--+-- >>> toNatural 0+-- 0+--+-- >>> toNatural 2+-- 2+--+-- >>> toNatural $ S $ S $ Z+-- 2+--+toNatural :: Nat -> Natural+toNatural Z = 0+toNatural (S n) = succ (toNatural n)++-- | Convert 'Natural' to 'Nat'+--+-- >>> fromNatural 4+-- 4+--+-- >>> explicitShow (fromNatural 4)+-- "S (S (S (S Z)))"+--+fromNatural :: Natural -> Nat+fromNatural 0 = Z+fromNatural n = S (fromNatural (pred n))++-------------------------------------------------------------------------------+-- Aliases+-------------------------------------------------------------------------------++nat0, nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9 :: Nat+nat0 = Z+nat1 = S nat0+nat2 = S nat1+nat3 = S nat2+nat4 = S nat3+nat5 = S nat4+nat6 = S nat5+nat7 = S nat6+nat8 = S nat7+nat9 = S nat8
+ src/Data/Type/Nat.hs view
@@ -0,0 +1,390 @@+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE GADTs                #-}+{-# LANGUAGE KindSignatures       #-}+{-# LANGUAGE RankNTypes           #-}+{-# LANGUAGE ScopedTypeVariables  #-}+{-# LANGUAGE StandaloneDeriving   #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE UndecidableInstances #-}+-- | 'Nat' numbers. @DataKinds@ stuff.+--+-- This module re-exports "Data.Nat", and adds type-level things.+module Data.Type.Nat (+    -- * Natural, Nat numbers+    Nat(..),+    toNatural,+    fromNatural,+    cata,+    -- * Showing+    explicitShow,+    explicitShowsPrec,+    -- * Singleton+    SNat(..),+    snatToNat,+    snatToNatural,+    -- * Implicit+    SNatI(..),+    reify,+    reflect,+    reflectToNum,+    -- * Equality+    eqNat,+    EqNat,+    -- * Induction+    induction,+    induction1,+    InlineInduction (..),+    inlineInduction,+    -- ** Example: unfoldedFix+    unfoldedFix,+    -- * Arithmetic+    Plus,+    Mult,+    -- * Conversion to GHC Nat+    ToGHC,+    FromGHC,+    -- * Aliases+    -- ** Nat+    nat0, nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9,+    -- ** promoted Nat+    Nat0, Nat1, Nat2, Nat3, Nat4, Nat5, Nat6, Nat7, Nat8, Nat9,+    -- * Proofs+    proofPlusZeroN,+    proofPlusNZero,+    proofMultZeroN,+    proofMultNZero,+    proofMultOneN,+    proofMultNOne,+    )  where++import Data.Function      (fix)+import Data.Nat+import Data.Proxy         (Proxy (..))+import Data.Type.Equality+import Numeric.Natural    (Natural)++import qualified GHC.TypeLits as GHC++import Unsafe.Coerce (unsafeCoerce)++-------------------------------------------------------------------------------+-- SNat+-------------------------------------------------------------------------------++-- | Singleton of 'Nat'.+data SNat (n :: Nat) where+    SZ :: SNat 'Z+    SS :: SNatI n => SNat ('S n)++deriving instance Show (SNat p)++-- | Convenience class to get 'SNat'.+class               SNatI (n :: Nat) where snat :: SNat n+instance            SNatI 'Z         where snat = SZ+instance SNatI n => SNatI ('S n)     where snat = SS++-- | Reflect type-level 'Nat' to the term level.+reflect :: forall n proxy. SNatI n => proxy n -> Nat+reflect _ = unTagged (induction1 (Tagged Z) (retagMap S) :: Tagged n Nat)++-- | As 'reflect' but with any 'Num'.+reflectToNum :: forall n m proxy. (SNatI n, Num m) => proxy n -> m+reflectToNum _ = unTagged (induction1 (Tagged 0) (retagMap (1+)) :: Tagged n m)++-- | Reify 'Nat'.+--+-- >>> reify nat3 reflect+-- 3+reify :: forall r. Nat -> (forall n. SNatI n => Proxy n -> r) -> r+reify Z     f = f (Proxy :: Proxy 'Z)+reify (S n) f =  reify n (\(_p :: Proxy n) -> f (Proxy :: Proxy ('S n)))++-- | Convert 'SNat' to 'Nat'.+--+-- >>> snatToNat (snat :: SNat Nat1)+-- 1+--+snatToNat :: forall n. SNat n -> Nat+snatToNat SZ = Z+snatToNat SS = unTagged (induction1 (Tagged Z) (retagMap S) :: Tagged n Nat)++-- | Convert 'SNat' to 'Natural'+--+-- >>> snatToNatural (snat :: SNat Nat0)+-- 0+--+-- >>> snatToNatural (snat :: SNat Nat2)+-- 2+--+snatToNatural :: forall n. SNat n -> Natural+snatToNatural SZ = 0+snatToNatural SS = unTagged (induction1 (Tagged 0) (retagMap succ) :: Tagged n Natural)++-------------------------------------------------------------------------------+-- Equality+-------------------------------------------------------------------------------++-- | Decide equality of type-level numbers.+--+-- >>> eqNat :: Maybe (Nat3 :~: Plus Nat1 Nat2)+-- Just Refl+--+-- >>> eqNat :: Maybe (Nat3 :~: Mult Nat2 Nat2)+-- Nothing+--+eqNat :: forall n m. (SNatI n, SNatI m) => Maybe (n :~: m)+eqNat = getNatEq $ induction (NatEq start) (\p -> NatEq (step p)) where+    start :: forall p. SNatI p => Maybe ('Z :~: p)+    start = case snat :: SNat p of+        SZ -> Just Refl+        SS -> Nothing++    step :: forall p q. SNatI q => NatEq p -> Maybe ('S p :~: q)+    step hind = case snat :: SNat q of+        SZ -> Nothing+        SS -> step' hind++    step' :: forall p q. SNatI q => NatEq p -> Maybe ('S p :~: 'S q)+    step' (NatEq hind) = do+        Refl <- hind :: Maybe (p :~: q)+        return Refl++newtype NatEq n = NatEq { getNatEq :: forall m. SNatI m => Maybe (n :~: m) }++instance TestEquality SNat where+    testEquality SZ SZ = Just Refl+    testEquality SZ SS = Nothing+    testEquality SS SZ = Nothing+    testEquality SS SS = eqNat++-- | Type family used to implement 'Data.Type.Equality.==' from "Data.Type.Equality" module.+type family EqNat (n :: Nat) (m :: Nat) where+    EqNat 'Z     'Z     = 'True+    EqNat ('S n) ('S m) = EqNat n m+    EqNat n      m      = 'False++type instance n == m = EqNat n m++-------------------------------------------------------------------------------+-- Induction+-------------------------------------------------------------------------------++-- | Induction on 'Nat', functor form. Useful for computation.+--+-- >>> induction1 (Tagged 0) $ retagMap (+2) :: Tagged Nat3 Int+-- Tagged 6+--+induction1+    :: forall n f a. SNatI n+    => f 'Z a                                      -- ^ zero case+    -> (forall m. SNatI m => f m a -> f ('S m) a)  -- ^ induction step+    -> f n a+induction1 z f = go where+    go :: forall m. SNatI m => f m a+    go = case snat :: SNat m of+        SZ -> z+        SS -> f go++-- | Induction on 'Nat'.+--+-- Useful in proofs or with GADTs, see source of 'proofPlusNZero'.+induction+    :: forall n f. SNatI n+    => f 'Z                                    -- ^ zero case+    -> (forall m. SNatI m => f m -> f ('S m))  -- ^ induction step+    -> f n+induction z f = go where+    go :: forall m. SNatI m => f m+    go = case snat :: SNat m of+        SZ -> z+        SS -> f go++-- | The induction will be fully inlined.+--+-- See @test/Inspection.hs@.+class SNatI n => InlineInduction (n :: Nat) where+    inlineInduction1 :: f 'Z a -> (forall m. InlineInduction m => f m a -> f ('S m) a) -> f n a++instance InlineInduction 'Z where+    inlineInduction1 z _ = z++instance InlineInduction n => InlineInduction ('S n) where+    inlineInduction1 z f = f (inlineInduction1 z f)++    -- Specialise this to few first numerals.+    {-# SPECIALIZE instance InlineInduction ('S 'Z) #-}+    {-# SPECIALIZE instance InlineInduction ('S ('S 'Z)) #-}+    {-# SPECIALIZE instance InlineInduction ('S ('S ('S 'Z))) #-}+    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S 'Z)))) #-}+    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S 'Z))))) #-}+    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S 'Z)))))) #-}+    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S ('S 'Z))))))) #-}+    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) #-}+    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) #-}++-- | See 'InlineInduction'.+inlineInduction+    :: forall n f. InlineInduction n+    => f 'Z                                              -- ^ zero case+    -> (forall m. InlineInduction m => f m -> f ('S m))  -- ^ induction step+    -> f n+inlineInduction z f = unConst' $ inlineInduction1 (Const' z) (Const' . f . unConst')++newtype Const' (f :: Nat -> *) (n :: Nat) a = Const' { unConst' :: f n }++-- | Unfold @n@ steps of a general recursion.+--+-- /Note:/ Always __benchmark__. This function may give you both /bad/ properties:+-- a lot of code (increased binary size), and worse performance.+--+-- For known @n@ 'unfoldedFix' will unfold recursion, for example+--+-- @+-- 'unfoldedFix' ('Proxy' :: 'Proxy' 'Nat3') f = f (f (f (fix f)))+-- @+--+unfoldedFix :: forall n a proxy. InlineInduction n => proxy n -> (a -> a) -> a+unfoldedFix _ = getFix (inlineInduction1 start step :: Fix n a) where+    start :: Fix 'Z a+    start = Fix fix++    step :: Fix m a -> Fix ('S m) a+    step (Fix go) = Fix $ \f -> f (go f)++newtype Fix (n :: Nat) a = Fix { getFix :: (a -> a) -> a }++-------------------------------------------------------------------------------+-- Conversion to GHC Nat+-------------------------------------------------------------------------------++-- | Convert to GHC 'GHC.Nat'.+--+-- >>> :kind! ToGHC Nat5+-- ToGHC Nat5 :: GHC.Nat+-- = 5+--+type family ToGHC (n :: Nat) :: GHC.Nat where+    ToGHC 'Z     = 0+    ToGHC ('S n) = 1 GHC.+ ToGHC n++-- | Convert from GHC 'GHC.Nat'.+--+-- >>> :kind! FromGHC 7+-- FromGHC 7 :: Nat+-- = 'S ('S ('S ('S ('S ('S ('S 'Z))))))+--+type family FromGHC (n :: GHC.Nat) :: Nat where+    FromGHC 0 = 'Z+    FromGHC n = 'S (FromGHC (n GHC.- 1))++-------------------------------------------------------------------------------+-- Arithmetic+-------------------------------------------------------------------------------++-- | Addition.+--+-- >>> reflect (snat :: SNat (Plus Nat1 Nat2))+-- 3+type family Plus (n :: Nat) (m :: Nat) :: Nat where+    Plus 'Z     m = m+    Plus ('S n) m = 'S (Plus n m)++-- | Multiplication.+--+-- >>> reflect (snat :: SNat (Mult Nat2 Nat3))+-- 6+type family Mult (n :: Nat) (m :: Nat) :: Nat where+    Mult 'Z     m = 'Z+    Mult ('S n) m = Plus m (Mult n m)++-------------------------------------------------------------------------------+-- Aliases+-------------------------------------------------------------------------------++type Nat0  = 'Z+type Nat1  = 'S Nat0+type Nat2  = 'S Nat1+type Nat3  = 'S Nat2+type Nat4  = 'S Nat3+type Nat5  = 'S Nat4+type Nat6  = 'S Nat5+type Nat7  = 'S Nat6+type Nat8  = 'S Nat7+type Nat9  = 'S Nat8++-------------------------------------------------------------------------------+-- proofs+-------------------------------------------------------------------------------++-- | @0 + n = n@+proofPlusZeroN :: Plus Nat0 n :~: n+proofPlusZeroN = Refl++-- | @n + 0 = n@+proofPlusNZero :: SNatI n => Plus n Nat0 :~: n+proofPlusNZero = getProofPlusNZero $ induction (ProofPlusNZero Refl) step where+    step :: forall m. ProofPlusNZero m -> ProofPlusNZero ('S m)+    step (ProofPlusNZero Refl) = ProofPlusNZero Refl++{-# NOINLINE [1] proofPlusNZero #-}+{-# RULES "Nat: n + 0 = n" proofPlusNZero = unsafeCoerce (Refl :: () :~: ()) #-}++newtype ProofPlusNZero n = ProofPlusNZero { getProofPlusNZero :: Plus n Nat0 :~: n }++-- TODO: plusAssoc++-- | @0 * n = 0@+proofMultZeroN :: Mult Nat0 n :~: Nat0+proofMultZeroN = Refl++-- | @n * 0 = n@+proofMultNZero :: forall n proxy. SNatI n => proxy n -> Mult n Nat0 :~: Nat0+proofMultNZero _ =+    getProofMultNZero (induction (ProofMultNZero Refl) step :: ProofMultNZero n)+  where+    step :: forall m. ProofMultNZero m -> ProofMultNZero ('S m)+    step (ProofMultNZero Refl) = ProofMultNZero Refl++{-# NOINLINE [1] proofMultNZero #-}+{-# RULES "Nat: n * 0 = n" proofMultNZero = unsafeCoerce (Refl :: () :~: ()) #-}++newtype ProofMultNZero n = ProofMultNZero { getProofMultNZero :: Mult n Nat0 :~: Nat0 }++-- | @1 * n = n@+proofMultOneN :: SNatI n => Mult Nat1 n :~: n+proofMultOneN = proofPlusNZero++{-# NOINLINE [1] proofMultOneN #-}+{-# RULES "Nat: 1 * n = n" proofMultOneN = unsafeCoerce (Refl :: () :~: ()) #-}++-- | @n * 1 = n@+proofMultNOne :: SNatI n => Mult n Nat1 :~: n+proofMultNOne = getProofMultNOne $ induction (ProofMultNOne Refl) step where+    step :: forall m. ProofMultNOne m -> ProofMultNOne ('S m)+    step (ProofMultNOne Refl) = ProofMultNOne Refl++{-# NOINLINE [1] proofMultNOne #-}+{-# RULES "Nat: n * 1 = n" proofMultNOne = unsafeCoerce (Refl :: () :~: ()) #-}++newtype ProofMultNOne n = ProofMultNOne { getProofMultNOne :: Mult n Nat1 :~: n }++-- TODO: multAssoc++-------------------------------------------------------------------------------+-- Tagged+-------------------------------------------------------------------------------++-- Own 'Tagged', to not depend on @tagged@+--+-- We shouldn't export this in public interface.+newtype Tagged (n :: Nat) a = Tagged a deriving Show++unTagged :: Tagged n a -> a+unTagged (Tagged a) = a++retagMap :: (a -> b) -> Tagged n a -> Tagged m b+retagMap f = Tagged . f . unTagged++-- $setup+-- >>> :set -XTypeOperators -XDataKinds
+ test/Inspection.hs view
@@ -0,0 +1,113 @@+{-# LANGUAGE DeriveGeneric       #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell     #-}+{-# LANGUAGE TypeOperators       #-}+{-# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin #-}+module Main (main) where++import Data.Function      (fix)+import Data.Proxy         (Proxy (..))+import Data.Tagged        (Tagged (..), retag)+import Data.Type.Equality+import GHC.Generics       (Generic)+import Test.Inspection++import qualified Data.Fin      as F+import qualified Data.Fin.Enum as E+import qualified Data.Type.Nat as N++import Unsafe.Coerce (unsafeCoerce)++-------------------------------------------------------------------------------+-- InlineInduction+-------------------------------------------------------------------------------++-- | This doesn't evaluate compile time.+lhsInline :: Int+lhsInline = unTagged (N.inlineInduction1 (pure 0) (retag . fmap succ) :: Tagged N.Nat5 Int)++-- | This doesn't evaluate compile time.+lhsNormal :: Int+lhsNormal = unTagged (N.induction1 (pure 0) (retag . fmap succ) :: Tagged N.Nat5 Int)++rhs :: Int+rhs = 5++inspect $ 'lhsInline === 'rhs+inspect $ 'lhsNormal =/= 'rhs++-------------------------------------------------------------------------------+-- Enum+-------------------------------------------------------------------------------++-- | Note: GHC 8.0 (but not GHC 8.2?) seems to be+-- so smart, it reuses dictionary value.+--+-- Therefore, we define own local Ordering'+data Ordering' = LT' | EQ' | GT' deriving (Generic)++lhsEnum :: Ordering' -> F.Fin N.Nat3+lhsEnum = E.gfrom++rhsEnum :: Ordering' -> F.Fin N.Nat3+rhsEnum LT' = F.Z+rhsEnum EQ' = F.S F.Z+rhsEnum GT' = F.S (F.S F.Z)++inspect $ 'lhsEnum ==- 'rhsEnum++-------------------------------------------------------------------------------+-- Proofs+-------------------------------------------------------------------------------++lhsProof :: forall n. N.SNatI n => F.Fin (N.Mult n N.Nat1) -> F.Fin n+lhsProof x = case N.proofMultNOne :: N.Mult n N.Nat1 :~: n of+    Refl -> x++rhsProof :: forall n. N.SNatI n => F.Fin (N.Mult n N.Nat1) -> F.Fin n+rhsProof x = unsafeCoerce x++inspect $ 'lhsProof ==- 'rhsProof++-------------------------------------------------------------------------------+-- unfoldedFix+-------------------------------------------------------------------------------++foldrF :: (a -> b -> b) -> b -> ([a] -> b) -> [a] -> b+foldrF _f  z _go []     = z+foldrF  f _z  go (x : xs) = f x (go xs)++superfold :: [Int] -> Int+superfold = N.unfoldedFix (Proxy :: Proxy N.Nat5) (foldrF (+) 0)++-- Note: we need to write list explicitly, cannot use shorthand [1..4]+-- 'enumFromTo' is a recursive function!+--+-- Try to change [1,2,4,] to [1..4] to see the generated core :)+lhsFold :: Int+lhsFold = superfold [1,2,3,4]++lhsFold' :: Int+lhsFold' = fix (foldrF (+) 0) [1,2,3,4]++rhsFold :: Int+rhsFold = 10++inspect $ 'lhsFold  === 'rhsFold+inspect $ 'lhsFold' =/= 'rhsFold++lhsUnfold :: (a -> a) -> a+lhsUnfold f = N.unfoldedFix (Proxy :: Proxy N.Nat3) f++rhsUnfold :: (a -> a) -> a+rhsUnfold f = f (f (f (fix f)))++inspect $  'lhsUnfold === 'rhsUnfold++-------------------------------------------------------------------------------+-- Main to make GHC happy+-------------------------------------------------------------------------------++main :: IO ()+main = return ()