Last active
July 27, 2023 00:06
-
-
Save kana-sama/9185b30b45bd9817f11361e424a8abc7 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE DataKinds #-} | |
| {-# LANGUAGE GADTs #-} | |
| {-# LANGUAGE PolyKinds #-} | |
| {-# LANGUAGE RankNTypes #-} | |
| {-# LANGUAGE StandaloneKindSignatures #-} | |
| {-# LANGUAGE TypeApplications #-} | |
| {-# LANGUAGE TypeFamilies #-} | |
| {-# LANGUAGE TypeOperators #-} | |
| {-# LANGUAGE UndecidableInstances #-} | |
| {-# LANGUAGE NoStarIsType #-} | |
| import Data.Type.Equality ((:~:) (..)) | |
| import qualified GHC.TypeLits as GHC (Nat, type (+), type (-)) | |
| -- Equality | |
| type (==) = (:~:) | |
| infix 4 == | |
| type Reverse :: a == b -> b == a | |
| type family Reverse p where | |
| Reverse Refl = Refl | |
| type (>>) :: a == b -> b == c -> a == c | |
| type family a >> b where | |
| Refl >> Refl = Refl | |
| infixr 9 >> | |
| type (<<) :: b == a -> b == c -> a == c | |
| type a << b = Reverse a >> b | |
| infixr 9 << | |
| type Cong :: forall a b f. a == b -> f a == f b | |
| type family Cong p where | |
| Cong Refl = Refl | |
| type (@@) :: forall a b. forall f -> a == b -> f a == f b | |
| type f @@ (p :: a == b) = Cong @a @b @f p | |
| infixr 0 @@ | |
| -- Nat | |
| data Nat where | |
| Zero :: Nat | |
| Succ :: Nat -> Nat | |
| type FromNat :: GHC.Nat -> Nat | |
| type family FromNat n where | |
| FromNat 0 = Zero | |
| FromNat n = Succ (FromNat (n GHC.- 1)) | |
| type ToNat :: Nat -> GHC.Nat | |
| type family ToNat n where | |
| ToNat Zero = 0 | |
| ToNat (Succ x) = ToNat x GHC.+ 1 | |
| type (+) :: Nat -> Nat -> Nat | |
| type family a + b where | |
| Zero + b = b | |
| Succ a + b = Succ (a + b) | |
| infixl 6 + | |
| type (*) :: Nat -> Nat -> Nat | |
| type family a * b where | |
| Zero * _ = Zero | |
| Succ a * b = b + (a * b) | |
| infixl 7 * | |
| -- Nat properties | |
| type Plus_Zero_Right :: forall a -> a + Zero == a | |
| type family Plus_Zero_Right a where | |
| Plus_Zero_Right Zero = Refl | |
| Plus_Zero_Right (Succ n) = Succ @@ Plus_Zero_Right n | |
| type Plus_Shift_Right :: forall a b -> Succ a + b == a + Succ b | |
| type family Plus_Shift_Right a b where | |
| Plus_Shift_Right Zero _ = Refl | |
| Plus_Shift_Right (Succ a) b = Succ @@ Plus_Shift_Right a b | |
| type Plus_Left :: forall a b. forall c -> a == b -> c + a == c + b | |
| type family Plus_Left c p where | |
| Plus_Left _ Refl = Refl | |
| type Plus_Right :: forall a b. forall c -> a == b -> a + c == b + c | |
| type family Plus_Right c p where | |
| Plus_Right _ Refl = Refl | |
| type Plus_Assoc :: forall a b c -> (a + b) + c == a + (b + c) | |
| type family Plus_Assoc a b c where | |
| Plus_Assoc Zero _ _ = Refl | |
| Plus_Assoc (Succ a) b c = Succ @@ Plus_Assoc a b c | |
| type Plus_Commute :: forall a b -> a + b == b + a | |
| type family Plus_Commute a b where | |
| Plus_Commute Zero b = Reverse (Plus_Zero_Right b) | |
| Plus_Commute (Succ a) b = (Succ @@ Plus_Commute a b) >> Plus_Shift_Right b a | |
| type Mult_Zero_Right :: forall a -> a * Zero == Zero | |
| type family Mult_Zero_Right a where | |
| Mult_Zero_Right Zero = Refl | |
| Mult_Zero_Right (Succ a) = Mult_Zero_Right a | |
| type Plus_Mult :: forall a b -> a + a * b == a * Succ b | |
| type family Plus_Mult a b where | |
| Plus_Mult Zero _ = Refl | |
| Plus_Mult (Succ a) b = Succ @@ Plus_Assoc a b (a * b) << Plus_Right (a * b) (Plus_Commute a b) >> Plus_Assoc b a (a * b) >> Plus_Left b (Plus_Mult a b) | |
| type Mult_Commute :: forall a b -> a * b == b * a | |
| type family Mult_Commute a b where | |
| Mult_Commute Zero b = Reverse (Mult_Zero_Right b) | |
| Mult_Commute (Succ a) b = Plus_Left b (Mult_Commute a b) >> Plus_Mult b a |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment