| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
DependentLiterals.Int
Description
The library component of DependentLiterals.Plugin.
This provides a class for dependent numeric literal functionality, the entry points used by the plugin for literals and patterns, and a few ways of defining instances with less unsafe-ty.
Synopsis
- class HasIntLiterals a where
- type ReprAssertion a :: Type -> Integer -> Constraint
- type LitConstraint a :: Integer -> Constraint
- type LitAssertion a :: Type -> Integer -> Constraint
- unsafeFromInteger :: forall n b. (LitAssertion a b n, ReprAssertion a b n) => Proxy b -> Tagged n Integer -> a
- unsafeMatchInteger :: forall n b. ReprAssertion a b n => Proxy b -> Tagged n Integer -> a -> CMaybe (LitConstraint a n)
- valueOf :: forall n a. (IntLiteral (ToInteger n) a, KnownInteger (ToInteger n)) => a
- type HasBasicLiterals a = (HasIntLiterals a, LitAssertion a ~ NoAssertion, ReprAssertion a ~ NoAssertion)
- type AllowsIntLiteral n a = (LitAssertion a a (ToInteger n), ReprAssertion a a (ToInteger n))
- type IntLiteral n a = (HasIntLiterals a, AllowsIntLiteral n a)
- newtype StockLit a = StockLit a
- class SNum a where
- type SNumRepr a :: Type
- type SNumConstraint a :: Integer -> Constraint
- fromSNum :: Satisfying (SNumConstraint a) (SNumber (SNumRepr a)) -> a
- intoSNum :: a -> Satisfying (SNumConstraint a) (SNumber (SNumRepr a))
- data Satisfying c t = forall x.c x => Satisfying (t x)
- newtype SNumLit (c :: Type -> Integer -> Constraint) a = SNumLit a
- type family (m :: Nat) -# (n :: Nat) :: Integer where ...
- data CMaybe c
- lit# :: forall n a. (HasIntLiterals a, ReprAssertion a a n, LitAssertion a a n) => (Num a => a) -> Integer -> a
- match# :: forall n a. (HasIntLiterals a, ReprAssertion a a n) => (Num a => a) -> Integer -> a -> CMaybe (LitConstraint a n)
- class NoAssertion (a :: Type) (n :: Integer)
Dependent Literals
class HasIntLiterals a where Source #
The main class providing dependent-literals functionality.
Instances of this can have integral literals and numeric patterns with
-fplugin=DependentLiterals.Plugin.
This class exposes the internal unsafe machinery of the library; a safer and
less error-prone way to get instances for it is via SNum or StockLit.
Associated Types
type ReprAssertion a :: Type -> Integer -> Constraint Source #
Constraint for representational validity of a literal: this is meant to
prevent overflowed literals from being wrapped incorrectly in N#. This
is required both for expressions and for patterns.
Safety contract: unsafeFromInteger and unsafeMatchInteger must not
construct illegal SNumber n values when called with Tagged @n n; they
may use ReprAssertion to restrict the values they can receive.
type LitConstraint a :: Integer -> Constraint Source #
LitConstraint a n constrains or refines a given the literal value.
This is what's proven about the integer value and type by matching on a
numeric pattern; for example, in the case of SInt n, LitConstraint a m
is m ~ n, so that matching numeric SInt patterns introduces equality
proofs for the type parameter.
type LitAssertion a :: Type -> Integer -> Constraint Source #
Like LitConstraint but with pretty error messages.
This is used on integral literals to provide custom error messages for failed constraints.
Methods
unsafeFromInteger :: forall n b. (LitAssertion a b n, ReprAssertion a b n) => Proxy b -> Tagged n Integer -> a Source #
Runtime conversion from Integer to the appropriate type.
Unsafe in that it trusts that the Integer you give it is the same as the
type-level one.
unsafeMatchInteger :: forall n b. ReprAssertion a b n => Proxy b -> Tagged n Integer -> a -> CMaybe (LitConstraint a n) Source #
Runtime pattern match implementation.
Unsafe in that it trusts that the Integer you give it is the same as the
type-level one.
Instances
valueOf :: forall n a. (IntLiteral (ToInteger n) a, KnownInteger (ToInteger n)) => a Source #
Get the value of a type-level number at runtime, as if it were a literal.
That is, when DependentLiterals is enabled, 42 and valueOf @42 are the
same thing. (When it's not enabled, 42 is just fromInteger 42).
Convenience Aliases
type HasBasicLiterals a = (HasIntLiterals a, LitAssertion a ~ NoAssertion, ReprAssertion a ~ NoAssertion) Source #
A constraint alias that asserts you can use any integral literal.
This can be useful in polymorphic contexts when you don't want to list out constraints for every literal value you need, and are willing to accept that some types with stronger compile-time validation will be excluded.
type AllowsIntLiteral n a = (LitAssertion a a (ToInteger n), ReprAssertion a a (ToInteger n)) Source #
A constraint alias showing that the particular value n is valid for a.
With this in context along with HasIntLiterals an at type a. See also IntLiteral.
type IntLiteral n a = (HasIntLiterals a, AllowsIntLiteral n a) Source #
A convenient form of IntLiteral when only one value is needed.
This is a constraint tuple, so using this multiple times in a signature
creates a bit of constraint pollution; for tidier signatures, use one
HasIntLiterals and several AllowsIntLiterals.
Safer Implementations
Use Wrapped Num
The HasIntLiterals instance of Wrapped NumNum instance.
For use with -XDerivingVia. This calls through to the fromIntegral of
the underlying Num instance for the final conversion. If the type in
question has a Num instance and it's acceptable for literals to overflow
(or if the type is supported by -Woverflowed-literals), this is a good way
to get an instance.
This is suitable for DerivingVia and tends to work as a deriving clause,
so:
newtype MyType = MyType Int
deriving (Eq, Num)
deriving HasIntLiterals via Wrapped Num MyType
Note in this case you could just as well say deriving HasIntLiterals to
get a GeneralizedNewtypeDeriving instance that consumes Int literals and
coerces them, but if you wrote a custom Num instance, via Wrapped Num MyType
will respect it.
Constructors
| StockLit a |
Instances
| (Eq a, Num a) => HasIntLiterals (StockLit a) Source # | |
Defined in DependentLiterals.Int Associated Types type ReprAssertion (StockLit a) :: Type -> Integer -> Constraint Source # type LitConstraint (StockLit a) :: Integer -> Constraint Source # type LitAssertion (StockLit a) :: Type -> Integer -> Constraint Source # Methods unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (StockLit a) b n, ReprAssertion (StockLit a) b n) => Proxy b -> Tagged n Integer -> StockLit a Source # unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (StockLit a) b n => Proxy b -> Tagged n Integer -> StockLit a -> CMaybe (LitConstraint (StockLit a) n) Source # | |
| type ReprAssertion (StockLit a) Source # | |
Defined in DependentLiterals.Int | |
| type LitConstraint (StockLit a) Source # | |
Defined in DependentLiterals.Int | |
| type LitAssertion (StockLit a) Source # | |
Defined in DependentLiterals.Int | |
A user-facing dependent numeric typeclass.
This gives an isomorphism between a and exists n. SNumber (SNumRepr a) n
given that SNumConstraint a n holds.
To get instances of HasIntLiterals without interacting with the unsafe
parts of the library, implement this class and lift it to HasIntLiterals
with deriving HasIntLiterals via SNumLit MyAssertionClass MyType.
Associated Types
type SNumRepr a :: Type Source #
The underlying numerical representation type.
type SNumConstraint a :: Integer -> Constraint Source #
The constraint on literal values to validate/refine a.
Methods
fromSNum :: Satisfying (SNumConstraint a) (SNumber (SNumRepr a)) -> a Source #
Conversion from SNumber with a proof of SNumConstraint into a.
Used for interpreting integral literals.
intoSNum :: a -> Satisfying (SNumConstraint a) (SNumber (SNumRepr a)) Source #
Conversion from a into SNumber with a proof of 'SNumConstraint.'
Used for providing proofs on successful pattern matches.
Instances
data Satisfying c t Source #
A GADT containing some t x along with a c x instance.
Constructors
| forall x.c x => Satisfying (t x) |
newtype SNumLit (c :: Type -> Integer -> Constraint) a Source #
A newtype carrying a HasIntLiterals instance for use with DerivingVia.
Constructors
| SNumLit a |
Instances
| (Eq (SNumRepr a), Num (SNumRepr a), SNum a) => HasIntLiterals (SNumLit c a) Source # | |
Defined in DependentLiterals.Int Associated Types type ReprAssertion (SNumLit c a) :: Type -> Integer -> Constraint Source # type LitConstraint (SNumLit c a) :: Integer -> Constraint Source # type LitAssertion (SNumLit c a) :: Type -> Integer -> Constraint Source # Methods unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (SNumLit c a) b n, ReprAssertion (SNumLit c a) b n) => Proxy b -> Tagged n Integer -> SNumLit c a Source # unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (SNumLit c a) b n => Proxy b -> Tagged n Integer -> SNumLit c a -> CMaybe (LitConstraint (SNumLit c a) n) Source # | |
| type ReprAssertion (SNumLit c a) Source # | |
Defined in DependentLiterals.Int | |
| type LitConstraint (SNumLit c a) Source # | |
Defined in DependentLiterals.Int | |
| type LitAssertion (SNumLit c a) Source # | |
Defined in DependentLiterals.Int | |
Plugin Entry Points
lit# :: forall n a. (HasIntLiterals a, ReprAssertion a a n, LitAssertion a a n) => (Num a => a) -> Integer -> a Source #
The unsafe entry point used by DependentLiterals.Plugin for literals.
This is unsafe to use explicitly, since it implicitly trusts that the given
Integer is equal to the type-level integer. The plugin guarantees this
itself when generating calls, so its uses are safe.
match# :: forall n a. (HasIntLiterals a, ReprAssertion a a n) => (Num a => a) -> Integer -> a -> CMaybe (LitConstraint a n) Source #
The unsafe entry point used by DependentLiterals.Plugin for patterns.
This is unsafe to use explicitly, since it implicitly trusts that the given
Integer is equal to the type-level integer. The plugin guarantees this
itself when generating calls, so its uses are safe.
Implementation Details
class NoAssertion (a :: Type) (n :: Integer) Source #
The "assertion" used by basic integral literals, which is always solvable.
Instances
| NoAssertion a n Source # | |
Defined in DependentLiterals.Int | |