-
Notifications
You must be signed in to change notification settings - Fork 39
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Showing
4 changed files
with
170 additions
and
3 deletions.
There are no files selected for viewing
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,40 @@ | ||
<!-- | ||
A new scriv changelog fragment. | ||
Uncomment the section that is right (remove the HTML comment wrapper). | ||
--> | ||
|
||
<!-- | ||
### Removed | ||
- A bullet item for the Removed category. | ||
--> | ||
### Added | ||
|
||
- `DBType` instance for `Fixed` that would map (e.g.) `Micro` to `numeric(1000, 6)` and `Pico` to `numeric(1000, 12)`. | ||
|
||
<!-- | ||
### Changed | ||
- A bullet item for the Changed category. | ||
--> | ||
<!-- | ||
### Deprecated | ||
- A bullet item for the Deprecated category. | ||
--> | ||
<!-- | ||
### Fixed | ||
- A bullet item for the Fixed category. | ||
--> | ||
<!-- | ||
### Security | ||
- A bullet item for the Security category. | ||
--> |
This file contains 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
This file contains 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
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,103 @@ | ||
{-# language AllowAmbiguousTypes #-} | ||
{-# language ConstraintKinds #-} | ||
{-# language DataKinds #-} | ||
{-# language FlexibleContexts #-} | ||
{-# language FlexibleInstances #-} | ||
{-# language NoStarIsType #-} | ||
{-# language PolyKinds #-} | ||
{-# language RankNTypes #-} | ||
{-# language ScopedTypeVariables #-} | ||
{-# language StandaloneKindSignatures #-} | ||
{-# language TypeApplications #-} | ||
{-# language TypeFamilies #-} | ||
{-# language TypeOperators #-} | ||
{-# language UndecidableInstances #-} | ||
|
||
module Rel8.Type.Decimal | ||
( PowerOf10 | ||
, resolution | ||
) | ||
where | ||
|
||
-- base | ||
import Data.Fixed (E0, E1, E2, E3, E6, E9, E12, HasResolution) | ||
import Data.Proxy (Proxy (Proxy)) | ||
import Data.Type.Equality (type (==)) | ||
import Data.Type.Ord (type (<?)) | ||
import Data.Kind (Constraint) | ||
import GHC.TypeLits (ErrorMessage ((:<>:), ShowType, Text), TypeError) | ||
import GHC.TypeNats (KnownNat, Nat, type (+), type (-), type (*), Div, natVal) | ||
import Numeric.Natural (Natural) | ||
import Prelude | ||
|
||
|
||
type PowerOf10 :: a -> Constraint | ||
class (HasResolution n, KnownNat (Log n)) => PowerOf10 n where | ||
type Log n :: Nat | ||
|
||
|
||
instance (KnownNat n, KnownNat (Log n), IsPowerOf10 n) => PowerOf10 n where | ||
type Log n = Log10 n | ||
|
||
|
||
instance PowerOf10 E0 where | ||
type Log E0 = 0 | ||
|
||
|
||
instance PowerOf10 E1 where | ||
type Log E1 = 1 | ||
|
||
|
||
instance PowerOf10 E2 where | ||
type Log E2 = 2 | ||
|
||
|
||
instance PowerOf10 E3 where | ||
type Log E3 = 3 | ||
|
||
|
||
instance PowerOf10 E6 where | ||
type Log E6 = 6 | ||
|
||
|
||
instance PowerOf10 E9 where | ||
type Log E9 = 9 | ||
|
||
|
||
instance PowerOf10 E12 where | ||
type Log E12 = 12 | ||
|
||
|
||
resolution :: forall n. PowerOf10 n => Natural | ||
resolution = natVal (Proxy @(Log n)) | ||
|
||
|
||
type Exp10 :: Nat -> Nat | ||
type Exp10 n = Exp10' 1 n | ||
|
||
|
||
type Exp10' :: Nat -> Nat -> Nat | ||
type family Exp10' x n where | ||
Exp10' x 0 = x | ||
Exp10' x n = Exp10' (x * 10) (n - 1) | ||
|
||
|
||
type Log10 :: Nat -> Nat | ||
type Log10 n = Log10' (n <? 10) n | ||
|
||
|
||
type Log10' :: Bool -> Nat -> Nat | ||
type family Log10' bool n where | ||
Log10' 'True _n = 0 | ||
Log10' 'False n = 1 + Log10 (Div n 10) | ||
|
||
|
||
type IsPowerOf10 :: Nat -> Constraint | ||
type IsPowerOf10 n = IsPowerOf10' (Exp10 (Log10 n) == n) n | ||
|
||
|
||
type IsPowerOf10' :: Bool -> Nat -> Constraint | ||
type family IsPowerOf10' bool n where | ||
IsPowerOf10' 'True _n = () | ||
IsPowerOf10' 'False n = | ||
TypeError ('ShowType n ':<>: 'Text " is not a power of 10") |