dependent-literals-0.1.1.0: Provides library support for pseudo-dependently-typed int literals.
Safe HaskellNone
LanguageHaskell2010

DependentLiterals

Description

Top-level module exporting the key DependentLiterals functionality.

Synopsis

Int Literals

class HasIntLiterals a 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.

Minimal complete definition

unsafeFromInteger, unsafeMatchInteger

Instances

Instances details
HasIntLiterals Double Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals Float Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals Int Source # 
Instance details

Defined in DependentLiterals.Int

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion Int b n, ReprAssertion Int b n) => Proxy b -> Tagged n Integer -> Int Source #

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion Int b n => Proxy b -> Tagged n Integer -> Int -> CMaybe (LitConstraint Int n) Source #

HasIntLiterals Int8 Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals Int16 Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals Int32 Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals Int64 Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals Integer Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals Natural Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals Word Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals Word8 Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals Word16 Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals Word32 Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals Word64 Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CChar Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CSChar Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CUChar Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CShort Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CUShort Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CInt Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CUInt Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CLong Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CULong Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CLLong Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CULLong Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CBool Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CPtrdiff Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CSize Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CWchar Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CSigAtomic Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CClock Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CTime Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CUSeconds Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CSUSeconds Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CIntPtr Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CUIntPtr Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CIntMax Source # 
Instance details

Defined in DependentLiterals.Int

HasIntLiterals CUIntMax Source # 
Instance details

Defined in DependentLiterals.Int

Integral a => HasIntLiterals (Ratio a) Source # 
Instance details

Defined in DependentLiterals.Int

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (Ratio a) b n, ReprAssertion (Ratio a) b n) => Proxy b -> Tagged n Integer -> Ratio a Source #

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (Ratio a) b n => Proxy b -> Tagged n Integer -> Ratio a -> CMaybe (LitConstraint (Ratio a) n) Source #

(Eq a, Num a) => HasIntLiterals (Min a) Source # 
Instance details

Defined in DependentLiterals.Int

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (Min a) b n, ReprAssertion (Min a) b n) => Proxy b -> Tagged n Integer -> Min a Source #

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (Min a) b n => Proxy b -> Tagged n Integer -> Min a -> CMaybe (LitConstraint (Min a) n) Source #

(Eq a, Num a) => HasIntLiterals (Max a) Source # 
Instance details

Defined in DependentLiterals.Int

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (Max a) b n, ReprAssertion (Max a) b n) => Proxy b -> Tagged n Integer -> Max a Source #

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (Max a) b n => Proxy b -> Tagged n Integer -> Max a -> CMaybe (LitConstraint (Max a) n) Source #

(Eq a, Num a) => HasIntLiterals (Identity a) Source # 
Instance details

Defined in DependentLiterals.Int

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (Identity a) b n, ReprAssertion (Identity a) b n) => Proxy b -> Tagged n Integer -> Identity a Source #

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (Identity a) b n => Proxy b -> Tagged n Integer -> Identity a -> CMaybe (LitConstraint (Identity a) n) Source #

(Eq a, Num a) => HasIntLiterals (Sum a) Source # 
Instance details

Defined in DependentLiterals.Int

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (Sum a) b n, ReprAssertion (Sum a) b n) => Proxy b -> Tagged n Integer -> Sum a Source #

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (Sum a) b n => Proxy b -> Tagged n Integer -> Sum a -> CMaybe (LitConstraint (Sum a) n) Source #

(Eq a, Num a) => HasIntLiterals (Product a) Source # 
Instance details

Defined in DependentLiterals.Int

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (Product a) b n, ReprAssertion (Product a) b n) => Proxy b -> Tagged n Integer -> Product a Source #

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (Product a) b n => Proxy b -> Tagged n Integer -> Product a -> CMaybe (LitConstraint (Product a) n) Source #

HasIntLiterals (Fin n) Source # 
Instance details

Defined in DependentLiterals.Int

Methods

unsafeFromInteger :: forall (n0 :: Integer) b. (LitAssertion (Fin n) b n0, ReprAssertion (Fin n) b n0) => Proxy b -> Tagged n0 Integer -> Fin n Source #

unsafeMatchInteger :: forall (n0 :: Integer) b. ReprAssertion (Fin n) b n0 => Proxy b -> Tagged n0 Integer -> Fin n -> CMaybe (LitConstraint (Fin n) n0) Source #

HasIntLiterals (SInt n) Source # 
Instance details

Defined in DependentLiterals.Int

Methods

unsafeFromInteger :: forall (n0 :: Integer) b. (LitAssertion (SInt n) b n0, ReprAssertion (SInt n) b n0) => Proxy b -> Tagged n0 Integer -> SInt n Source #

unsafeMatchInteger :: forall (n0 :: Integer) b. ReprAssertion (SInt n) b n0 => Proxy b -> Tagged n0 Integer -> SInt n -> CMaybe (LitConstraint (SInt n) n0) Source #

(Eq a, Num a) => HasIntLiterals (StockLit a) Source # 
Instance details

Defined in DependentLiterals.Int

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 #

(Eq a, Num a) => HasIntLiterals (SNumber a n) Source # 
Instance details

Defined in DependentLiterals.Int

Methods

unsafeFromInteger :: forall (n0 :: Integer) b. (LitAssertion (SNumber a n) b n0, ReprAssertion (SNumber a n) b n0) => Proxy b -> Tagged n0 Integer -> SNumber a n Source #

unsafeMatchInteger :: forall (n0 :: Integer) b. ReprAssertion (SNumber a n) b n0 => Proxy b -> Tagged n0 Integer -> SNumber a n -> CMaybe (LitConstraint (SNumber a n) n0) Source #

(Eq a, Num a) => HasIntLiterals (Wrapped Num a) Source # 
Instance details

Defined in DependentLiterals.Int

Methods

unsafeFromInteger :: forall (n :: Integer) b. (LitAssertion (Wrapped Num a) b n, ReprAssertion (Wrapped Num a) b n) => Proxy b -> Tagged n Integer -> Wrapped Num a Source #

unsafeMatchInteger :: forall (n :: Integer) b. ReprAssertion (Wrapped Num a) b n => Proxy b -> Tagged n Integer -> Wrapped Num a -> CMaybe (LitConstraint (Wrapped Num a) n) Source #

(Eq (SNumRepr a), Num (SNumRepr a), SNum a) => HasIntLiterals (SNumLit c a) Source # 
Instance details

Defined in DependentLiterals.Int

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 #

(Eq a, Num a) => HasIntLiterals (Const a b) Source # 
Instance details

Defined in DependentLiterals.Int

Associated Types

type ReprAssertion (Const a b) :: Type -> Integer -> Constraint Source #

type LitConstraint (Const a b) :: Integer -> Constraint Source #

type LitAssertion (Const a b) :: Type -> Integer -> Constraint Source #

Methods

unsafeFromInteger :: forall (n :: Integer) b0. (LitAssertion (Const a b) b0 n, ReprAssertion (Const a b) b0 n) => Proxy b0 -> Tagged n Integer -> Const a b Source #

unsafeMatchInteger :: forall (n :: Integer) b0. ReprAssertion (Const a b) b0 n => Proxy b0 -> Tagged n Integer -> Const a b -> CMaybe (LitConstraint (Const a b) n) Source #

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 a, you can use an integral literal value n 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.

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).

Basic Literals

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.

newtype StockLit a Source #

Use Wrapped Num directly instead.

The HasIntLiterals instance of Wrapped Num results in integral literals and patterns that behave like the stock literals would have, according to the underlying type's Num 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

Instances details
(Eq a, Num a) => HasIntLiterals (StockLit a) Source # 
Instance details

Defined in DependentLiterals.Int

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 # 
Instance details

Defined in DependentLiterals.Int

type LitConstraint (StockLit a) Source # 
Instance details

Defined in DependentLiterals.Int

type LitAssertion (StockLit a) Source # 
Instance details

Defined in DependentLiterals.Int

Dependent Literals

class SNum a where Source #

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

Instances details
SNum (Fin n) Source # 
Instance details

Defined in DependentLiterals.Int

Associated Types

type SNumRepr (Fin n) Source #

type SNumConstraint (Fin n) :: Integer -> Constraint Source #

SNum (SInt n) Source # 
Instance details

Defined in DependentLiterals.Int

Associated Types

type SNumRepr (SInt n) Source #

type SNumConstraint (SInt n) :: Integer -> Constraint Source #

SNum (SNumber a n) Source # 
Instance details

Defined in DependentLiterals.Int

Associated Types

type SNumRepr (SNumber a n) Source #

type SNumConstraint (SNumber a n) :: Integer -> Constraint Source #

newtype SNumLit (c :: Type -> Integer -> Constraint) a Source #

A newtype carrying a HasIntLiterals instance for use with DerivingVia.

Constructors

SNumLit a 

Instances

Instances details
(Eq (SNumRepr a), Num (SNumRepr a), SNum a) => HasIntLiterals (SNumLit c a) Source # 
Instance details

Defined in DependentLiterals.Int

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 # 
Instance details

Defined in DependentLiterals.Int

type LitConstraint (SNumLit c a) Source # 
Instance details

Defined in DependentLiterals.Int

type LitAssertion (SNumLit c a) Source # 
Instance details

Defined in DependentLiterals.Int