Modulefirst-class-families-0.8.2.0Haskell2010

Fcf.Utils

Miscellaneous families.

13 types
1 class

Packagefirst-class-families-0.8.2.0
Exports17
LanguageHaskell2010
LicenceMIT
SourceUtils.hs

datadata Error (b :: Symbol) (c :: a)

Type-level error.

Instances1Eval

type Eval (Error msg) = TypeError ('Text msg)Defined in first-class-families-0.8.2.0 · Fcf.Utils

datadata TError (b :: ErrorMessage) (c :: a)

TypeError as a fcf.

Instances1Eval

type Eval (TError msg) = TypeError msgDefined in first-class-families-0.8.2.0 · Fcf.Utils

datadata Constraints (a :: [Constraint]) (b :: Constraint)

Conjunction of a list of constraints.

Instances2Eval

type Eval (Constraints '[]) = ()Defined in first-class-families-0.8.2.0 · Fcf.Utils
type Eval (Constraints (a ': as)) = (a, Eval (Constraints as))Defined in first-class-families-0.8.2.0 · Fcf.Utils

datadata TyEq (c :: a) (d :: b) (e :: Bool)

Type equality.

Details

The base library also defines a similar (Type.Equality.==); 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.

Instances1Eval

type Eval (TyEq a b) = TyEqImpl a bDefined in first-class-families-0.8.2.0 · Fcf.Utils

familytype family Stuck :: a

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

classclass IsBool (b :: Bool) where

Methods

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

Instances2IsBool

IsBool 'FalseDefined in first-class-families-0.8.2.0 · Fcf.Utils
IsBool 'TrueDefined in first-class-families-0.8.2.0 · Fcf.Utils

datadata Case (a :: [Match j k]) (b :: j) (c :: k)

(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)
  ]

Instances1Eval

type Eval (Case ms a) = Case_ ms aDefined in first-class-families-0.8.2.0 · Fcf.Utils

datadata Match j k

typetype (-->) = 'Match_

Match concrete type in Case.

typetype Is = 'Is_

Match on predicate being successful with type in Case.

typetype Any = 'Any_

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.

typetype Else = 'Else_

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

From Data.Type.Bool

1 declaration

familytype 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 fls = tru
If 'False tru fls = fls

Compile-time asserts

2 declarations

datadata Assert (a :: ErrorMessage) (b :: Exp Bool) (c :: r) (d :: r)

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

Instances1Eval

type Eval (Assert msg mcond k) = Eval (If (Eval mcond) (Pure k) (TError msg))Defined in first-class-families-0.8.2.0 · Fcf.Utils

datadata AssertNot (a :: ErrorMessage) (b :: Exp Bool) (c :: r) (d :: r)

Compile-time assert, with condition negated.

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

Also see Assert.

Instances1Eval

type Eval (AssertNot err mcond k) = Eval (Assert err (Not =<< mcond) k)Defined in first-class-families-0.8.2.0 · Fcf.Utils

Reexports

2 declarations

datadata ErrorMessage

A description of a custom type error.

Constructors

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

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