From 2b6265672109542e51d8364dc46d503e85a4311d Mon Sep 17 00:00:00 2001 From: mniip Date: Thu, 14 Dec 2017 12:12:21 +0300 Subject: [PATCH] Initial commit --- GHC/TypeLits/Induction.hs | 87 ++++++++++++++++++ GHC/TypeLits/Singletons.hs | 184 +++++++++++++++++++++++++++++++++++++ LICENSE | 30 ++++++ Setup.hs | 2 + singleton-typelits.cabal | 17 ++++ 5 files changed, 320 insertions(+) create mode 100644 GHC/TypeLits/Induction.hs create mode 100644 GHC/TypeLits/Singletons.hs create mode 100644 LICENSE create mode 100644 Setup.hs create mode 100644 singleton-typelits.cabal diff --git a/GHC/TypeLits/Induction.hs b/GHC/TypeLits/Induction.hs new file mode 100644 index 0000000..56ec5b5 --- /dev/null +++ b/GHC/TypeLits/Induction.hs @@ -0,0 +1,87 @@ +-- | +-- Module : GHC.TypeLits.Induction +-- Description : Induction for GHC TypeLits +-- Copyright : (C) 2017 mniip +-- License : MIT +-- Maintainer : mniip@mniip.com +-- Stability : experimental +-- Portability : portable +{-# LANGUAGE TypeOperators, KindSignatures, DataKinds, PolyKinds, GADTs, RankNTypes, StandaloneDeriving, InstanceSigs, ScopedTypeVariables #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} + +module GHC.TypeLits.Induction + ( + -- * Natural number induction + induceIsZero, + inducePeano, + induceTwosComp, + induceBaseComp, + + -- * Positive number induction + induceUnary, + inducePosBinary, + inducePosBase + ) + where + +import Data.Proxy +import GHC.TypeLits +import GHC.TypeLits.Singletons + +-- | \((\forall n. n > 0 \to P(n)) \to P(0) \to \forall m. P(m)\) +induceIsZero :: KnownNat m => (forall n. KnownNat n => p (1 + n)) -> p 0 -> p m +induceIsZero = go natSingleton + where + go :: NatIsZero m -> (forall n. KnownNat n => p (1 + n)) -> p 0 -> p m + go IsZero y z = z + go IsNonZero y z = y + +-- | \((\forall n. P(n) \to P(n + 1)) \to P(0) \to \forall m. P(m)\) +inducePeano :: KnownNat m => (forall n. KnownNat n => p n -> p (1 + n)) -> p 0 -> p m +inducePeano = go natSingleton + where + go :: NatPeano m -> (forall n. KnownNat n => p n -> p (1 + n)) -> p 0 -> p m + go PeanoZero f z = z + go (PeanoSucc n) f z = f (go n f z) + +-- | \((\forall n. P(n) \to P(2n + 1)) \to \\ (\forall n. P(n) \to P(2n + 2)) \to \\ P(0) \to \\ \forall m. P(m)\) +induceTwosComp :: KnownNat m => (forall n. KnownNat n => p n -> p (1 + 2 * n)) -> (forall n. KnownNat n => p n -> p (2 + 2 * n)) -> p 0 -> p m +induceTwosComp = go natSingleton + where + go :: NatTwosComp m -> (forall n. KnownNat n => p n -> p (1 + 2 * n)) -> (forall n. KnownNat n => p n -> p (2 + 2 * n)) -> p 0 -> p m + go TwosCompZero f g z = z + go (TwosCompx2p1 n) f g z = f (go n f g z) + go (TwosCompx2p2 n) f g z = g (go n f g z) + +-- | \(\forall b. (\prod_d Q(d)) \to \\ (\forall n. \forall d. d < b \to Q(d) \to P(n) \to P(bn + d + 1)) \to \\ \forall m. P(m)\) +induceBaseComp :: forall r b q p m. (KnownNat b, KnownNat m) => r b -> (forall m. KnownNat m => q m) -> (forall k n. (KnownNat b, 1 + k <= b, KnownNat n) => q k -> p n -> p (1 + k + b * n)) -> p 0 -> p m +induceBaseComp _ = go natSingleton + where + go :: forall m. NatBaseComp Proxy b m -> (forall m. (KnownNat m, 1 + m <= b) => q m) -> (forall k n. (KnownNat b, 1 + k <= b, KnownNat n) => q k -> p n -> p (1 + k + b * n)) -> p 0 -> p m + go BaseCompZero q f z = z + go (BaseCompxBp1p k n) q f z = f q (go n q f z) + +-- | \((\forall n. P(n) \to P(n + 1)) \to P(1) \to \forall m > 0. P(m)\) +induceUnary :: KnownNat m => (forall n. KnownNat n => p n -> p (1 + n)) -> p 1 -> p (1 + m) +induceUnary = go posSingleton + where + go :: Unary m -> (forall n. KnownNat n => p n -> p (1 + n)) -> p 1 -> p m + go UnaryOne f o = o + go (UnarySucc n) f o = f (go n f o) + +-- | \((\forall n. P(n) \to P(2n)) \to \\ (\forall n. P(n) \to P(2n + 1)) \to \\ P(1) \to \\ \forall m > 0. P(m)\) +inducePosBinary :: KnownNat m => (forall n. KnownNat n => p n -> p (2 * n)) -> (forall n. KnownNat n => p n -> p (1 + 2 * n)) -> p 1 -> p (1 + m) +inducePosBinary = go posSingleton + where + go :: PosBinary m -> (forall n. KnownNat n => p n -> p (2 * n)) -> (forall n. KnownNat n => p n -> p (1 + 2 * n)) -> p 1 -> p m + go BinOne f g z = z + go (Bin0 n) f g z = f (go n f g z) + go (Bin1 n) f g z = g (go n f g z) + +-- | \(\forall b. (\prod_d Q(d)) \to \\ (\forall n. \forall d. d < b \to Q(d) \to P(n) \to P(bn + d)) \to \\ (\forall d. d > 0 \to d < b \to Q(d) \to P(d)) \to \\ \forall m > 0. P (m)\) +inducePosBase :: forall r b q p m. (KnownNat b, KnownNat m) => r b -> (forall m. KnownNat m => q m) -> (forall k n. (KnownNat b, 1 + k <= b, KnownNat n) => q k -> p n -> p (k + b * n)) -> (forall k n. (KnownNat k, 1 + k <= b, k ~ (1 + n)) => q k -> p k) -> p (1 + m) +inducePosBase _ = go posSingleton + where + go :: forall m. PosBase Proxy b m -> (forall m. KnownNat m => q m) -> (forall k n. (KnownNat b, 1 + k <= b, KnownNat n) => q k -> p n -> p (k + b * n)) -> (forall k n. (KnownNat k, 1 + k <= b, k ~ (1 + n)) => q k -> p k) -> p m + go (BaseLead n) q f g = g q + go (BaseDigit k n) q f g = f q (go n q f g) diff --git a/GHC/TypeLits/Singletons.hs b/GHC/TypeLits/Singletons.hs new file mode 100644 index 0000000..1a146cf --- /dev/null +++ b/GHC/TypeLits/Singletons.hs @@ -0,0 +1,184 @@ +-- | +-- Module : GHC.TypeLits.Singletons +-- Description : Singletons for GHC TypeLits +-- Copyright : (C) 2017 mniip +-- License : MIT +-- Maintainer : mniip@mniip.com +-- Stability : experimental +-- Portability : portable +{-# LANGUAGE TypeOperators, KindSignatures, DataKinds, PolyKinds, GADTs, RankNTypes, StandaloneDeriving, InstanceSigs, ScopedTypeVariables #-} +{-# OPTIONS_GHC -fno-warn-tabs #-} + +module GHC.TypeLits.Singletons + ( + -- * Natural number singletons + NatSingleton(..), + NatIsZero(..), + NatPeano(..), + NatTwosComp(..), + NatBaseComp(..), + + -- * Positive number singleton + PositiveSingleton(..), + Unary(..), + PosBinary(..), + PosBase(..), + + ShowN(..) + ) + where + +import GHC.TypeLits +import Data.Type.Equality +import Unsafe.Coerce +import Data.Proxy + +-- | A class of singletons capable of representing any 'KnownNat' natural number. +class NatSingleton (p :: Nat -> *) where + natSingleton :: KnownNat n => p n + +-- | Auxiliary class for implementing 'Show' on higher-kinded singletons. +class ShowN (p :: Nat -> *) where showsPrecN :: Int -> p n -> ShowS + +instance ShowN Proxy where showsPrecN = showsPrec + +instance NatSingleton Proxy where + natSingleton = Proxy + +-- | A natural number is either 0 or 1 plus something. +data NatIsZero (n :: Nat) where + IsZero :: NatIsZero 0 + IsNonZero :: KnownNat n => NatIsZero (1 + n) +deriving instance Show (NatIsZero n) +instance ShowN NatIsZero where showsPrecN = showsPrec + +instance NatSingleton NatIsZero where + natSingleton :: forall n. KnownNat n => NatIsZero n + natSingleton = case natVal (Proxy :: Proxy n) of + 0 -> (unsafeCoerce :: NatIsZero 0 -> NatIsZero n) IsZero + n -> case someNatVal (n - 1) of + Just (SomeNat (p :: Proxy m)) -> (unsafeCoerce :: NatIsZero (1 + m) -> NatIsZero n) $ IsNonZero + Nothing -> error $ "Malformed KnownNat instance: " ++ show n + +-- | A natural number is either 0 or a successor of another natural number. +data NatPeano (n :: Nat) where + PeanoZero :: NatPeano 0 + PeanoSucc :: KnownNat n => NatPeano n -> NatPeano (1 + n) +deriving instance Show (NatPeano n) +instance ShowN NatPeano where showsPrecN = showsPrec + +instance NatSingleton NatPeano where + natSingleton :: forall n. KnownNat n => NatPeano n + natSingleton = case natSingleton :: NatIsZero n of + IsZero -> PeanoZero + IsNonZero -> PeanoSucc natSingleton + +-- | A natural number is either 0, or twice another natural number plus 1 or 2. +data NatTwosComp (n :: Nat) where + TwosCompZero :: NatTwosComp 0 + TwosCompx2p1 :: KnownNat n => NatTwosComp n -> NatTwosComp (1 + 2 * n) + TwosCompx2p2 :: KnownNat n => NatTwosComp n -> NatTwosComp (2 + 2 * n) +deriving instance Show (NatTwosComp n) +instance ShowN NatTwosComp where showsPrecN = showsPrec + +instance NatSingleton NatTwosComp where + natSingleton :: forall n. KnownNat n => NatTwosComp n + natSingleton = case natVal (Proxy :: Proxy n) of + 0 -> (unsafeCoerce :: NatTwosComp 0 -> NatTwosComp n) TwosCompZero + n -> case someNatVal ((n - 1) `div` 2) of + Just (SomeNat (p :: Proxy m)) -> if even n + then (unsafeCoerce :: NatTwosComp (2 + 2 * m) -> NatTwosComp n) $ TwosCompx2p2 natSingleton + else (unsafeCoerce :: NatTwosComp (1 + 2 * m) -> NatTwosComp n) $ TwosCompx2p1 natSingleton + Nothing -> error $ "Malformed KnownNat instance: " ++ show n + +-- | A natural number is either 0, or @b@ times another natural number plus a digit in @[1, b]@. +data NatBaseComp (p :: Nat -> *) (b :: Nat) (n :: Nat) where + BaseCompZero :: NatBaseComp p b 0 + BaseCompxBp1p :: (KnownNat k, 1 + k <= b, KnownNat n) => p k -> NatBaseComp p b n -> NatBaseComp p b (1 + k + b * n) +instance ShowN p => Show (NatBaseComp p b n) where + showsPrec d BaseCompZero = showString "BaseCompZero" + showsPrec d (BaseCompxBp1p a b) = showParen (d > 10) $ showString "BaseCompxBp1p " . showsPrecN 11 a . showString " " . showsPrec 11 b +instance ShowN p => ShowN (NatBaseComp p b) where showsPrecN = showsPrec + +instance (KnownNat b, NatSingleton p) => NatSingleton (NatBaseComp p b) where + natSingleton :: forall n. KnownNat n => NatBaseComp p b n + natSingleton = case natVal (Proxy :: Proxy n) of + 0 -> (unsafeCoerce :: NatBaseComp p b 0 -> NatBaseComp p b n) BaseCompZero + n -> case someNatVal ((n - 1) `div` base) of + Just (SomeNat (p :: Proxy m)) -> case someNatVal ((n - 1) `mod` base) of + Just (SomeNat (p :: Proxy k)) -> (unsafeCoerce :: NatBaseComp p b (1 + k + b * m) -> NatBaseComp p b n) $ case unsafeCoerce Refl :: (1 + k <=? b) :~: True of + Refl -> BaseCompxBp1p (natSingleton :: p k) (natSingleton :: NatBaseComp p b m) + Nothing -> error $ "Malformed KnownNat instance: " ++ show base + Nothing -> error $ "Malformed KnownNat instance: " ++ show n + where + base = natVal (Proxy :: Proxy b) + +-- | A class of singletons capable of representing postive 'KnownNat' natural numbers. +class PositiveSingleton (p :: Nat -> *) where + posSingleton :: KnownNat n => p (1 + n) + +instance PositiveSingleton Proxy where + posSingleton = Proxy + +-- | A positive number is either 1 or a successor of another positive number. +data Unary (n :: Nat) where + UnaryOne :: Unary 1 + UnarySucc :: KnownNat n => Unary n -> Unary (1 + n) +deriving instance Show (Unary n) +instance ShowN Unary where showsPrecN = showsPrec + +instance PositiveSingleton Unary where + posSingleton :: forall n. KnownNat n => Unary (1 + n) + posSingleton = case natSingleton :: NatIsZero n of + IsZero -> UnaryOne + IsNonZero -> UnarySucc posSingleton + +-- | A positive number is either 1, or twice another positive number plus 0 or 1. +data PosBinary (n :: Nat) where + BinOne :: PosBinary 1 + Bin0 :: KnownNat n => PosBinary n -> PosBinary (2 * n) + Bin1 :: KnownNat n => PosBinary n -> PosBinary (1 + 2 * n) +deriving instance Show (PosBinary n) +instance ShowN PosBinary where showsPrecN = showsPrec + +instance PositiveSingleton PosBinary where + posSingleton :: forall n. KnownNat n => PosBinary (1 + n) + posSingleton = case natVal (Proxy :: Proxy n) of + 0 -> (unsafeCoerce :: PosBinary 1 -> PosBinary (1 + n)) BinOne + n -> case someNatVal ((n - 1) `div` 2) of + Just (SomeNat (p :: Proxy m)) -> case someNatVal (natVal (Proxy :: Proxy m) + 1) of + Just (SomeNat (q :: Proxy l)) -> case unsafeCoerce Refl :: l :~: 1 + m of + Refl -> if even n + then (unsafeCoerce :: PosBinary (1 + 2 * l) -> PosBinary (1 + n)) $ Bin1 posSingleton + else (unsafeCoerce :: PosBinary (2 * l) -> PosBinary (1 + n)) $ Bin0 posSingleton + Nothing -> error $ "Malformed KnownNat instance: " ++ show n + Nothing -> error $ "Malformed KnownNat instance: " ++ show n + +-- | A positive number is either a digit in @[1, b)@, or another positive number times @b@ plus a digit in @[0, b)@. +data PosBase (p :: Nat -> *) (b :: Nat) (n :: Nat) where + BaseLead :: (KnownNat k, 1 + k <= b, k ~ (1 + n)) => p k -> PosBase p b k + BaseDigit :: (KnownNat k, 1 + k <= b, KnownNat n) => p k -> PosBase p b n -> PosBase p b (k + b * n) +instance ShowN p => Show (PosBase p b n) where + showsPrec d (BaseLead a) = showParen (d > 10) $ showString "BaseLead " . showsPrecN 11 a + showsPrec d (BaseDigit a b) = showParen (d > 10) $ showString "BaseDigit " . showsPrecN 11 a . showString " " . showsPrec 11 b +instance ShowN p => ShowN (PosBase p b) where showsPrecN = showsPrec + +instance (KnownNat b, NatSingleton p) => PositiveSingleton (PosBase p b) where + posSingleton :: forall n. KnownNat n => PosBase p b (1 + n) + posSingleton = case natVal (Proxy :: Proxy n) of + n | n < base - 1 -> case someNatVal (n + 1) of + Just (SomeNat (p :: Proxy k)) -> case unsafeCoerce Refl :: k :~: (1 + n) of + Refl -> case unsafeCoerce Refl :: (1 + (1 + n) <=? b) :~: True of + Refl -> BaseLead natSingleton + Nothing -> error $ "Malformed KnownNat instance: " ++ show n + n -> case someNatVal ((n - base + 1) `div` base) of + Just (SomeNat (p :: Proxy m)) -> case someNatVal (natVal (Proxy :: Proxy m) + 1) of + Just (SomeNat (q :: Proxy l)) -> case unsafeCoerce Refl :: l :~: 1 + m of + Refl -> case someNatVal ((n - base + 1) `mod` base) of + Just (SomeNat (p :: Proxy k)) -> (unsafeCoerce :: PosBase p b (k + b * l) -> PosBase p b (1 + n)) $ case unsafeCoerce Refl :: (1 + k <=? b) :~: True of + Refl -> BaseDigit (natSingleton :: p k) (posSingleton :: PosBase p b l) + Nothing -> error $ "Malformed KnownNat instance: " ++ show base + Nothing -> error $ "Malformed KnownNat instance: " ++ show base + Nothing -> error $ "Malformed KnownNat instance: " ++ show n + where + base = natVal (Proxy :: Proxy b) diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..450ec63 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2017, mniip + +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 mniip 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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 index 0000000..9a994af --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/singleton-typelits.cabal b/singleton-typelits.cabal new file mode 100644 index 0000000..4994375 --- /dev/null +++ b/singleton-typelits.cabal @@ -0,0 +1,17 @@ +name: singleton-typelits +version: 0.0.0.0 +synopsis: Singletons and induction over GHC TypeLits +description: Singletons and induction schemes over 'GHC.TypeLits.Nat' +homepage: https://github.com/mniip/singleton-typelits +license: BSD3 +license-file: LICENSE +author: mniip +maintainer: mniip@mniip.com +category: Data +build-type: Simple +cabal-version: >=1.10 + +library + exposed-modules: GHC.TypeLits.Singletons, GHC.TypeLits.Induction + build-depends: base >=4.9 && <4.11 + default-language: Haskell2010