Safe Haskell	Safe-Inferred
Language	Haskell2010

Fcf.Utils

Contents

From Data.Type.Bool
Compile-time asserts
Reexports

Description

Miscellaneous families.

Synopsis

data Error (b :: Symbol) (c :: a)
data TError (b :: ErrorMessage) (c :: a)
data Constraints (a :: [Constraint]) b
data TyEq (c :: a) (d :: b) (e :: Bool)
type family Stuck :: a
class IsBool (b :: Bool) where
- _If :: (b ~ 'True => r) -> (b ~ 'False => r) -> r
data Case (a :: [Match j k]) (b :: j) (c :: k)
data Match j k
type (-->) = 'Match_ :: j -> k -> Match j k
type Is = 'Is_ :: (j -> Exp Bool) -> k -> Match j k
type Any = 'Any_ :: k -> Match j k
type Else = 'Else_ :: (j -> Exp k) -> Match j k
type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ...
data Assert (a :: ErrorMessage) (b :: Exp Bool) (c :: r) (d :: r)
data AssertNot (a :: ErrorMessage) (b :: Exp Bool) (c :: r) (d :: r)
data ErrorMessage
- = Text Symbol
- | ShowType t
- | ErrorMessage :<>: ErrorMessage
- | ErrorMessage :$$: ErrorMessage
type family TypeError (a :: ErrorMessage) :: b where ...

Documentation

data Error (b :: Symbol) (c :: a) Source #

Type-level error.

Instances

Instances details

type Eval (Error msg :: a -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (Error msg :: a -> Type) = TypeError ('Text msg) :: a

data TError (b :: ErrorMessage) (c :: a) Source #

TypeError as a fcf.

Instances

Instances details

type Eval (TError msg :: a -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (TError msg :: a -> Type) = TypeError msg :: a

data Constraints (a :: [Constraint]) b Source #

Conjunction of a list of constraints.

Instances

Instances details

type Eval (Constraints (a ': as) :: Constraint -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (Constraints (a ': as) :: Constraint -> Type) = (a, Eval (Constraints as))
type Eval (Constraints ('[] :: [Constraint])) Source #
Instance details Defined in Fcf.Utils type Eval (Constraints ('[] :: [Constraint])) = ()

data TyEq (c :: a) (d :: b) (e :: Bool) Source #

Type equality.

Details

Expand

The base library also defines a similar (==); it differs from TyEq in the following ways:

TyEq is heterogeneous: its arguments may have different kinds;
TyEq is reflexive: TyEq a a always reduces to True even if a is a variable.

Instances

Instances details

type Eval (TyEq a b :: Bool -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (TyEq a b :: Bool -> Type)

type family Stuck :: a Source #

A stuck type that can be used like a type-level undefined.

class IsBool (b :: Bool) where Source #

Methods

_If :: (b ~ 'True => r) -> (b ~ 'False => r) -> r Source #

Instances

Instances details

IsBool 'False Source #
Instance details Defined in Fcf.Utils Methods _If :: ('False ~ 'True => r) -> ('False ~ 'False => r) -> r Source #
IsBool 'True Source #
Instance details Defined in Fcf.Utils Methods _If :: ('True ~ 'True => r) -> ('True ~ 'False => r) -> r Source #

data Case (a :: [Match j k]) (b :: j) (c :: k) Source #

(Limited) equivalent of \case { .. } syntax. Supports matching of exact values (-->) and final matches for any value (Any) or for passing value to subcomputation (Else). Examples:

type BoolToNat = Case
  [ 'True  --> 0
  , 'False --> 1
  ]

type NatToBool = Case
  [ 0 --> 'False
  , Any   'True
  ]

type ZeroOneOrSucc = Case
  [ 0  --> 0
  , 1  --> 1
  , Else   ((+) 1)
  ]

Instances

Instances details

type Eval (Case ms a :: k -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (Case ms a :: k -> Type)

data Match j k Source #

type (-->) = 'Match_ :: j -> k -> Match j k infix 0 Source #

Match concrete type in Case.

type Is = 'Is_ :: (j -> Exp Bool) -> k -> Match j k Source #

Match on predicate being successful with type in Case.

type Any = 'Any_ :: k -> Match j k Source #

Match any type in Case. Should be used as a final branch.

Note: this identifier conflicts with Any (from Fcf.Class.Foldable) Any (from Data.Monoid), and Any (from GHC.Exts).

We recommend importing this one qualified.

type Else = 'Else_ :: (j -> Exp k) -> Match j k Source #

Pass type being matched in Case to subcomputation. Should be used as a final branch.

From Data.Type.Bool

type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ... #

Type-level If. If True a b ==> a; If False a b ==> b

Equations

If 'True (tru :: k) (fls :: k) = tru
If 'False (tru :: k) (fls :: k) = fls

Compile-time asserts

data Assert (a :: ErrorMessage) (b :: Exp Bool) (c :: r) (d :: r) Source #

A compile-time assert.

Raises the provided TypeError, whenever the condition evaluates to False.

Usage example: type ExampleAssertionFailure = Eval ( Pure '["foo", "bar"] >>= Length >>= Assert ('Text Assertion) (TyEq Int Void) )

Instances

Instances details

type Eval (Assert msg mcond k :: a -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (Assert msg mcond k :: a -> Type) = Eval (If (Eval mcond) (Pure k) (TError msg :: a -> Type))

data AssertNot (a :: ErrorMessage) (b :: Exp Bool) (c :: r) (d :: r) Source #

Compile-time assert, with condition negated.

Raises the provided TypeError, whenever the condition evaluates to True.

Also see Assert.

Instances

Instances details

type Eval (AssertNot err mcond k :: a -> Type) Source #
Instance details Defined in Fcf.Utils type Eval (AssertNot err mcond k :: a -> Type) = Eval (Assert err (Not =<< mcond) k)

Reexports

data ErrorMessage #

A description of a custom type error.

Constructors

Text Symbol	Show the text as is.
ShowType t	Pretty print the type. `ShowType :: k -> ErrorMessage`
ErrorMessage :<>: ErrorMessage infixl 6	Put two pieces of error message next to each other.
ErrorMessage :$$: ErrorMessage infixl 5	Stack two pieces of error message on top of each other.

type family TypeError (a :: ErrorMessage) :: b where ... #

The type-level equivalent of error.

The polymorphic kind of this type allows it to be used in several settings. For instance, it can be used as a constraint, e.g. to provide a better error message for a non-existent instance,

-- in a context
instance TypeError (Text "Cannot Show functions." :$$:
                    Text "Perhaps there is a missing argument?")
      => Show (a -> b) where
    showsPrec = error "unreachable"

It can also be placed on the right-hand side of a type-level function to provide an error for an invalid case,

type family ByteSize x where
   ByteSize Word16   = 2
   ByteSize Word8    = 1
   ByteSize a        = TypeError (Text "The type " :<>: ShowType a :<>:
                                  Text " is not exportable.")

Since: base-4.9.0.0