first-class-families-0.8.2.0: First-class type families

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 ... Source #

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 Source #

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 ... Source #

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