Created
December 4, 2025 01:07
-
-
Save tonymorris/435dc21721e7c02a8c95f1aa16813d8f 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
| {-# OPTIONS_GHC -Wall #-} | |
| {-# LANGUAGE DataKinds #-} | |
| {-# LANGUAGE GADTs #-} | |
| {-# LANGUAGE TypeFamilies #-} | |
| {-# LANGUAGE TypeOperators #-} | |
| {-# LANGUAGE ScopedTypeVariables #-} | |
| {-# LANGUAGE UndecidableInstances #-} | |
| {-# LANGUAGE FlexibleInstances #-} | |
| {-# LANGUAGE MultiParamTypeClasses #-} | |
| module Data.Natural where | |
| import Control.Lens | |
| import Data.Bool | |
| import Data.Proxy | |
| import GHC.TypeLits | |
| -- $setup | |
| -- | |
| -- >>> import Data.Foldable | |
| data NaturalNumber (n :: Nat) where | |
| NaturalNumber :: NaturalNumber n | |
| deriving (Eq, Ord, Show) | |
| naturalInteger :: | |
| forall n. KnownNat n => | |
| NaturalNumber n | |
| -> Integer | |
| naturalInteger _ = | |
| natVal (Proxy :: Proxy n) | |
| data SomeNaturalNumber where | |
| SomeNaturalNumber :: | |
| KnownNat n => | |
| NaturalNumber n | |
| -> SomeNaturalNumber | |
| instance Show SomeNaturalNumber where | |
| show (SomeNaturalNumber (NaturalNumber :: NaturalNumber n)) = | |
| show (natVal (Proxy :: Proxy n)) | |
| instance Eq SomeNaturalNumber where | |
| SomeNaturalNumber (NaturalNumber :: NaturalNumber n1) == SomeNaturalNumber (NaturalNumber :: NaturalNumber n2) = | |
| natVal (Proxy :: Proxy n1) == natVal (Proxy :: Proxy n2) | |
| instance Ord SomeNaturalNumber where | |
| compare (SomeNaturalNumber (NaturalNumber :: NaturalNumber n1)) (SomeNaturalNumber (NaturalNumber :: NaturalNumber n2)) = | |
| compare (natVal (Proxy :: Proxy n1)) (natVal (Proxy :: Proxy n2)) | |
| -- | | |
| -- | |
| -- >>> preview integerNatural 8 | |
| -- Just 8 | |
| -- | |
| -- >>> preview integerNatural 0 | |
| -- Just 0 | |
| -- | |
| -- >>> preview integerNatural (-1) | |
| -- Nothing | |
| -- | |
| -- >>> review integerNatural (SomeNaturalNumber (NaturalNumber :: NaturalNumber 0)) | |
| -- 0 | |
| -- | |
| -- >>> review integerNatural (SomeNaturalNumber (NaturalNumber :: NaturalNumber 1)) | |
| -- 1 | |
| integerNatural :: | |
| Prism' Integer SomeNaturalNumber | |
| integerNatural = | |
| prism' | |
| (\(SomeNaturalNumber (NaturalNumber :: NaturalNumber n)) -> natVal (Proxy :: Proxy n)) | |
| (\x -> | |
| let isNat = | |
| (\(SomeNat (_ :: Proxy n)) -> SomeNaturalNumber (NaturalNumber :: NaturalNumber n)) <$> someNatVal x | |
| in bool isNat Nothing (x < 0)) | |
| integerNaturalMultiply :: | |
| Prism' Integer MultiplySomeNaturalNumber | |
| integerNaturalMultiply = | |
| integerNatural . _Unwrapped | |
| -- | | |
| -- | |
| -- >>> plus (NaturalNumber :: NaturalNumber 2) (NaturalNumber :: NaturalNumber 3) == (NaturalNumber :: NaturalNumber 5) | |
| -- True | |
| plus :: | |
| NaturalNumber n | |
| -> NaturalNumber m | |
| -> NaturalNumber (n + m) | |
| plus _ _ = | |
| NaturalNumber | |
| -- | | |
| -- | |
| -- >>> SomeNaturalNumber (NaturalNumber :: NaturalNumber 2) <> SomeNaturalNumber (NaturalNumber :: NaturalNumber 3) | |
| -- 5 | |
| -- | |
| -- >>> fold (preview integerNatural <$> [1, 2, 3, 4, 5]) | |
| -- Just 15 | |
| -- | |
| -- >>> fold (preview integerNatural <$> [1, 2, 3, 4, 5, (-1)]) | |
| -- Just 15 | |
| -- | |
| -- >>> fold <$> traverse (preview integerNatural) [1, 2, 3, 4, 5] | |
| -- Just 15 | |
| -- | |
| -- >>> fold <$> traverse (preview integerNatural) [1, 2, 3, 4, 5, (-1)] | |
| -- Nothing | |
| instance Semigroup SomeNaturalNumber where | |
| SomeNaturalNumber n1 <> SomeNaturalNumber n2 = | |
| case someNatVal (natVal n1 + natVal n2) of | |
| Just (SomeNat (_ :: Proxy n)) -> | |
| SomeNaturalNumber (NaturalNumber :: NaturalNumber n) | |
| Nothing -> | |
| error "Impossible" | |
| instance Monoid SomeNaturalNumber where | |
| mempty = | |
| SomeNaturalNumber (NaturalNumber :: NaturalNumber 0) | |
| newtype MultiplySomeNaturalNumber = | |
| MultiplySomeNaturalNumber SomeNaturalNumber | |
| deriving (Eq, Ord, Show) | |
| instance (MultiplySomeNaturalNumber ~ a) => | |
| Rewrapped MultiplySomeNaturalNumber a | |
| instance Wrapped MultiplySomeNaturalNumber where | |
| type Unwrapped MultiplySomeNaturalNumber = | |
| SomeNaturalNumber | |
| _Wrapped' = | |
| iso (\ (MultiplySomeNaturalNumber x) -> x) | |
| MultiplySomeNaturalNumber | |
| -- | | |
| -- | |
| -- >>> fold (preview integerNaturalMultiply <$> [1, 2, 3, 4, 5]) | |
| -- Just (MultiplySomeNaturalNumber 120) | |
| -- | |
| -- >>> fold (preview integerNaturalMultiply <$> [1, 2, 3, 4, 5, (-1)]) | |
| -- Just (MultiplySomeNaturalNumber 120) | |
| -- | |
| -- >>> fold <$> traverse (preview integerNaturalMultiply) [1, 2, 3, 4, 5] | |
| -- Just (MultiplySomeNaturalNumber 120) | |
| -- | |
| -- >>> fold <$> traverse (preview integerNaturalMultiply) [1, 2, 3, 4, 5, (-1)] | |
| -- Nothing | |
| instance Semigroup MultiplySomeNaturalNumber where | |
| MultiplySomeNaturalNumber (SomeNaturalNumber n1) <> MultiplySomeNaturalNumber (SomeNaturalNumber n2) = | |
| MultiplySomeNaturalNumber ( | |
| case someNatVal (natVal n1 * natVal n2) of | |
| Just (SomeNat (_ :: Proxy n)) -> | |
| SomeNaturalNumber (NaturalNumber :: NaturalNumber n) | |
| Nothing -> | |
| error "Impossible" | |
| ) | |
| instance Monoid MultiplySomeNaturalNumber where | |
| mempty = | |
| MultiplySomeNaturalNumber (SomeNaturalNumber (NaturalNumber :: NaturalNumber 1)) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment