Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 18 additions & 0 deletions .github/workflows/restyled.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
name: Restyled

on:
pull_request:

concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true

jobs:
restyled:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: restyled-io/actions/setup@v4
- uses: restyled-io/actions/run@v4
with:
suggestions: true
4 changes: 4 additions & 0 deletions .restyled.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
restylers:
- fourmolu
- "!stylish-haskell"
- "*"
27 changes: 27 additions & 0 deletions fourmolu.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
indentation: 2
column-limit: 80 # needs fourmolu >= v0.12
function-arrows: leading
comma-style: leading # default
import-export-style: leading
import-grouping: # needs fourmolu >= v0.17
- name: "Preludes"
rules:
- glob: Prelude
- name: "Everything else"
rules:
- match: all
priority: 100
indent-wheres: false # default
record-brace-space: true
newlines-between-decls: 1 # default
haddock-style: single-line
let-style: mixed
in-style: left-align
single-constraint-parens: never # needs fourmolu >= v0.12
sort-constraints: true # needs fourmolu >= v0.17
sort-derived-classes: true # needs fourmolu >= v0.17
sort-derived-clauses: true # needs fourmolu >= v0.17
trailing-section-operators: false # needs fourmolu >= v0.17
unicode: never # default
respectful: true # default
fixities: null # default
2 changes: 1 addition & 1 deletion library/Closed.hs
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
module Closed
( Endpoint(..)
( Endpoint (..)
, Closed
, Bounds
, Single
Expand Down
146 changes: 92 additions & 54 deletions library/Closed/Internal.hs
Original file line number Diff line number Diff line change
Expand Up @@ -34,25 +34,26 @@ import GHC.Stack
import GHC.TypeLits
import Test.QuickCheck

newtype Closed (n :: Nat) (m :: Nat)
= Closed { getClosed :: Integer }
newtype Closed (a :: Nat) (b :: Nat) = Closed
{ getClosed :: Integer
}
deriving (Generic)

-- | Describe whether the endpoint of a 'Bounds' includes
-- or excludes its argument
data Endpoint
-- | Endpoint includes its argument
= Inclusive Nat
-- | Endpoint excludes its argument
| Exclusive Nat
= -- | Endpoint includes its argument
Inclusive Nat
| -- | Endpoint excludes its argument
Exclusive Nat

-- | Syntactic sugar to express open and half-open intervals using
-- the 'Closed' type
type family Bounds (lhs :: Endpoint) (rhs :: Endpoint) :: Type where
Bounds (Inclusive n) (Inclusive m) = Closed n m
Bounds (Inclusive n) (Exclusive m) = Closed n (m - 1)
Bounds (Exclusive n) (Inclusive m) = Closed (n + 1) m
Bounds (Exclusive n) (Exclusive m) = Closed (n + 1) (m - 1)
Bounds (Inclusive a) (Inclusive b) = Closed a b
Bounds (Inclusive a) (Exclusive b) = Closed a (b - 1)
Bounds (Exclusive a) (Inclusive b) = Closed (a + 1) b
Bounds (Exclusive a) (Exclusive b) = Closed (a + 1) (b - 1)

-- | Syntactic sugar to express a value that has only one non-bottom
-- inhabitant using the 'Closed' type
Expand All @@ -62,15 +63,19 @@ type Single (n :: Nat) = Bounds ('Inclusive n) ('Inclusive n)
type FiniteNat (rhs :: Endpoint) = Bounds ('Inclusive 0) rhs

-- | Proxy for the lower bound of a 'Closed' value
lowerBound :: Closed n m -> Proxy n
lowerBound :: Closed a b -> Proxy a
lowerBound _ = Proxy

-- | Proxy for the upper bound of a 'Closed' value
upperBound :: Closed n m -> Proxy m
upperBound :: Closed a b -> Proxy b
upperBound _ = Proxy

-- | Safely create a 'Closed' value using the specified argument
closed :: forall n m. (n <= m, KnownNat n, KnownNat m) => Integer -> Maybe (Closed n m)
closed
:: forall a b
. (KnownNat a, KnownNat b, a <= b)
=> Integer
-> Maybe (Closed a b)
closed x = result
where
extracted = fromJust result
Expand All @@ -79,7 +84,11 @@ closed x = result
pure $ Closed x

-- | Create a 'Closed' value throwing an error if the argument is not in range
unsafeClosed :: forall n m. (HasCallStack, n <= m, KnownNat n, KnownNat m) => Integer -> Closed n m
unsafeClosed
:: forall a b
. (HasCallStack, KnownNat a, KnownNat b, a <= b)
=> Integer
-> Closed a b
unsafeClosed x = result
where
result =
Expand All @@ -88,22 +97,26 @@ unsafeClosed x = result
else error $ unrepresentable x result "unsafeClosed"

-- | Clamp an @'Integral'@ in the range constrained by a @'Closed'@ interval
clamp :: forall n m a. (KnownNat n, KnownNat m, n <= m, Integral a) => a -> Closed n m
clamp
:: forall a b i
. (Integral i, KnownNat a, KnownNat b, a <= b)
=> i
-> Closed a b
clamp x
| fromIntegral x < getClosed (minBound @(Closed n m)) = minBound
| fromIntegral x > getClosed (maxBound @(Closed n m)) = maxBound
| fromIntegral x < getClosed (minBound @(Closed a b)) = minBound
| fromIntegral x > getClosed (maxBound @(Closed a b)) = maxBound
| otherwise = Closed (fromIntegral x)

-- | Test equality on 'Closed' values in the same range
instance Eq (Closed n m) where
instance Eq (Closed a b) where
Closed x == Closed y = x == y

-- | Compare 'Closed' values in the same range
instance Ord (Closed n m) where
instance Ord (Closed a b) where
Closed x `compare` Closed y = x `compare` y

-- | Generate the lowest and highest inhabitant of a given 'Closed' type
instance (n <= m, KnownNat n, KnownNat m) => Bounded (Closed n m) where
instance (KnownNat a, KnownNat b, a <= b) => Bounded (Closed a b) where
maxBound = result
where
result = Closed (natVal (upperBound result))
Expand All @@ -113,20 +126,20 @@ instance (n <= m, KnownNat n, KnownNat m) => Bounded (Closed n m) where
result = Closed (natVal (lowerBound result))

-- | Enumerate values in the range of a given 'Closed' type
instance (n <= m, KnownNat n, KnownNat m) => Enum (Closed n m) where
instance (KnownNat a, KnownNat b, a <= b) => Enum (Closed a b) where
fromEnum = fromEnum . getClosed
toEnum = unsafeClosed . toEnum
enumFrom x = enumFromTo x maxBound
enumFromThen x y = enumFromThenTo x y (if x >= y then minBound else maxBound)

instance Show (Closed n m) where
instance Show (Closed a b) where
showsPrec d (Closed x) = showParen (d > 9) $ showString "unsafeClosed " . showsPrec 10 x

-- | Bounded arithmetic, e.g. maxBound + 1 == maxBound
instance (n <= m, KnownNat n, KnownNat m) => Num (Closed n m) where
Closed x + Closed y = Closed $ min (x + y) (fromIntegral (maxBound :: Closed n m))
Closed x - Closed y = Closed $ max (x - y) (fromIntegral (minBound :: Closed n m))
Closed x * Closed y = Closed $ min (x * y) (fromIntegral (maxBound :: Closed n m))
instance (KnownNat a, KnownNat b, a <= b) => Num (Closed a b) where
Closed x + Closed y = Closed $ min (x + y) (fromIntegral (maxBound :: Closed a b))
Closed x - Closed y = Closed $ max (x - y) (fromIntegral (minBound :: Closed a b))
Closed x * Closed y = Closed $ min (x * y) (fromIntegral (maxBound :: Closed a b))
abs = id
signum = const 1
fromInteger x = result
Expand All @@ -136,114 +149,139 @@ instance (n <= m, KnownNat n, KnownNat m) => Num (Closed n m) where
then Closed x
else error $ unrepresentable x result "fromInteger"

instance (n <= m, KnownNat n, KnownNat m) => Real (Closed n m) where
instance (KnownNat a, KnownNat b, a <= b) => Real (Closed a b) where
toRational (Closed x) = x % 1

instance (n <= m, KnownNat n, KnownNat m) => Integral (Closed n m) where
instance (KnownNat a, KnownNat b, a <= b) => Integral (Closed a b) where
quotRem (Closed x) (Closed y) = (Closed $ x `quot` y, Closed $ x `rem` y)
toInteger (Closed x) = x

instance NFData (Closed n m)
instance NFData (Closed a b)

instance Hashable (Closed n m)
instance Hashable (Closed a b)

instance ToJSON (Closed n m) where
instance ToJSON (Closed a b) where
toEncoding = toEncoding . getClosed
toJSON = toJSON . getClosed

instance (n <= m, KnownNat n, KnownNat m) => FromJSON (Closed n m) where
instance (KnownNat a, KnownNat b, a <= b) => FromJSON (Closed a b) where
parseJSON v = do
x <- parseJSON v
case closed x of
Just cx -> pure cx
n -> fail $ unrepresentable x (fromJust n) "parseJSON"

instance CSV.ToField (Closed n m) where
instance CSV.ToField (Closed a b) where
toField = CSV.toField . getClosed

instance (n <= m, KnownNat n, KnownNat m) => CSV.FromField (Closed n m) where
instance (KnownNat a, KnownNat b, a <= b) => CSV.FromField (Closed a b) where
parseField s = do
x <- CSV.parseField s
case closed x of
Just cx -> pure cx
n -> fail $ unrepresentable x (fromJust n) "parseField"

instance (n <= m, KnownNat n, KnownNat m) => Arbitrary (Closed n m) where
instance (KnownNat a, KnownNat b, a <= b) => Arbitrary (Closed a b) where
arbitrary =
Closed <$> choose (natVal @n Proxy, natVal @m Proxy)
Closed <$> choose (natVal @a Proxy, natVal @b Proxy)

instance (n <= m, KnownNat n, KnownNat m) => PersistField (Closed n m) where
instance (KnownNat a, KnownNat b, a <= b) => PersistField (Closed a b) where
toPersistValue = toPersistValue . fromIntegral @Integer @Int . getClosed
fromPersistValue value = do
x <- fromIntegral @Int @Integer <$> fromPersistValue value
case closed @n @m x of
case closed @a @b x of
Just cx -> pure cx
n -> Left $ pack $ unrepresentable x (fromJust n) "fromPersistValue"

instance (n <= m, KnownNat n, KnownNat m) => PersistFieldSql (Closed n m) where
instance (KnownNat a, KnownNat b, a <= b) => PersistFieldSql (Closed a b) where
sqlType _ = sqlType (Proxy @Int)

unrepresentable :: (KnownNat n, KnownNat m) => Integer -> Closed n m -> String -> String
unrepresentable
:: (KnownNat a, KnownNat b)
=> Integer
-> Closed a b
-> String
-> String
unrepresentable x cx prefix =
prefix ++ ": Integer " ++ show x ++
" is not representable in Closed " ++ show (natVal $ lowerBound cx) ++
" " ++ show (natVal $ upperBound cx)
prefix
<> ": Integer "
<> show x
<> " is not representable in Closed "
<> show (natVal $ lowerBound cx)
<> " "
<> show (natVal $ upperBound cx)

-- | Convert a type-level literal into a 'Closed' value
natToClosed :: forall n m x proxy. (n <= x, x <= m, KnownNat x, KnownNat n, KnownNat m) => proxy x -> Closed n m
natToClosed
:: forall a b x proxy
. (KnownNat a, KnownNat b, KnownNat x, a <= x, x <= b)
=> proxy x
-> Closed a b
natToClosed p = Closed $ natVal p

-- | Add inhabitants at the end
weakenUpper :: forall k n m. (n <= m, m <= k) => Closed n m -> Closed n k
weakenUpper :: forall k a b. (a <= b, b <= k) => Closed a b -> Closed a k
weakenUpper (Closed x) = Closed x

-- | Add inhabitants at the beginning
weakenLower :: forall k n m. (n <= m, k <= n) => Closed n m -> Closed k m
weakenLower :: forall k a b. (a <= b, k <= a) => Closed a b -> Closed k b
weakenLower (Closed x) = Closed x

-- | Remove inhabitants from the end. Returns 'Nothing' if the input was removed
strengthenUpper :: forall k n m. (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed n k)
strengthenUpper
:: forall k a b
. (KnownNat a, KnownNat b, KnownNat k, a <= b, a <= k, k <= b)
=> Closed a b
-> Maybe (Closed a k)
strengthenUpper (Closed x) = result
where
result = do
guard $ x <= natVal (upperBound $ fromJust result)
pure $ Closed x

-- | Remove inhabitants from the beginning. Returns 'Nothing' if the input was removed
strengthenLower :: forall k n m. (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed k m)
strengthenLower
:: forall k a b
. (KnownNat a, KnownNat b, KnownNat k, a <= b, a <= k, k <= b)
=> Closed a b
-> Maybe (Closed k b)
strengthenLower (Closed x) = result
where
result = do
guard $ x >= natVal (lowerBound $ fromJust result)
pure $ Closed x

-- | Test two different types of 'Closed' values for equality.
equals :: Closed n m -> Closed o p -> Bool
equals :: Closed a b -> Closed o p -> Bool
equals (Closed x) (Closed y) = x == y

infix 4 `equals`

-- | Compare two different types of 'Closed' values
cmp :: Closed n m -> Closed o p -> Ordering
cmp :: Closed a b -> Closed o p -> Ordering
cmp (Closed x) (Closed y) = x `compare` y

-- | Add two different types of 'Closed' values
add :: Closed n m -> Closed o p -> Closed (n + o) (m + p)
add :: Closed a b -> Closed o p -> Closed (n + o) (m + p)
add (Closed x) (Closed y) = Closed $ x + y

-- | Subtract two different types of 'Closed' values
-- Returns 'Left' for negative results, and 'Right' for positive results.
sub :: Closed n m -> Closed o p -> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p))
sub
:: Closed a b
-> Closed o p
-> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p))
sub (Closed x) (Closed y)
| x >= y = Right $ Closed $ x - y
| otherwise = Left $ Closed $ y - x

-- | Multiply two different types of 'Closed' values
multiply :: Closed n m -> Closed o p -> Closed (n * o) (m * p)
multiply :: Closed a b -> Closed o p -> Closed (a * o) (b * p)
multiply (Closed x) (Closed y) = Closed $ x * y

-- | Verifies that a given 'Closed' value is valid.
-- Should always return 'True' unles you bring the @Closed.Internal.Closed@ constructor into scope,
-- or use 'Unsafe.Coerce.unsafeCoerce' or other nasty hacks
isValidClosed :: (KnownNat n, KnownNat m) => Closed n m -> Bool
isValidClosed :: (KnownNat a, KnownNat b) => Closed a b -> Bool
isValidClosed cx@(Closed x) =
natVal (lowerBound cx) <= x && x <= natVal (upperBound cx)
Loading