From 4ca302cdb32e3d36152400962cc50d37d3d40494 Mon Sep 17 00:00:00 2001 From: Mikolaj Konarski Date: Tue, 23 Apr 2024 16:54:09 +0200 Subject: Try to make up for ToINat not being injective --- src/Data/INat.hs | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) (limited to 'src/Data/INat.hs') diff --git a/src/Data/INat.hs b/src/Data/INat.hs index 7a495ca..2d65c53 100644 --- a/src/Data/INat.hs +++ b/src/Data/INat.hs @@ -13,9 +13,10 @@ module Data.INat where import Data.Proxy +import Data.Type.Equality ((:~:) (Refl)) import Numeric.Natural import GHC.TypeLits - +import Unsafe.Coerce (unsafeCoerce) -- | Evidence for the constraint @c a@. data Dict c a where @@ -73,10 +74,29 @@ type family FromINat n where FromINat (S n) = 1 + FromINat n -- | Convert a "GHC.TypeLits" 'G.Nat' to a 'INat'. -type family ToINat n where +type family ToINat (n :: Nat) where ToINat 0 = Z ToINat n = S (ToINat (n - 1)) +lemInjectiveFromINat :: n :~: ToINat (FromINat n) +lemInjectiveFromINat = unsafeCoerce Refl + +lemSuccFromINat :: Proxy n -> 1 + FromINat n :~: FromINat (S n) +lemSuccFromINat _ = unsafeCoerce Refl + +lemAddFromINat :: Proxy m -> Proxy n + -> FromINat m + FromINat n :~: FromINat (m +! n) +lemAddFromINat _ = unsafeCoerce Refl + +lemInjectiveToINat :: n :~: FromINat (ToINat n) +lemInjectiveToINat = unsafeCoerce Refl + +lemSuccToINat :: Proxy n -> ToINat (1 + n) :~: S (ToINat n) +lemSuccToINat _ = unsafeCoerce Refl + +lemAddToINat :: Proxy m -> Proxy n -> ToINat (m + n) :~: ToINat m +! ToINat n +lemAddToINat _ _ = unsafeCoerce Refl + -- | If an inductive 'INat' is known, then the corresponding "GHC.TypeLits" -- 'G.Nat' is also known. knownNatFromINat :: KnownINat n => Proxy n -> Dict KnownNat (FromINat n) -- cgit v1.2.3-70-g09d2