Safe Haskell	Safe
Language	Haskell2010

Fcf.Utils

Contents

From Data.Type.Bool

Description

Miscellaneous families.

Synopsis

data Error :: Symbol -> Exp a
data TError :: ErrorMessage -> Exp a
data Constraints :: [Constraint] -> Exp Constraint
data TyEq :: a -> b -> Exp Bool
type family Stuck :: a
class IsBool (b :: Bool) where
- _If :: (b ~ True => r) -> (b ~ False => r) -> r
data Case :: [Match j k] -> j -> Exp 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 ...

Documentation

data Error :: Symbol -> Exp a Source #

Type-level error.

Instances

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 :: ErrorMessage -> Exp a Source #

TypeError as a fcf.

Instances

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

data Constraints :: [Constraint] -> Exp Constraint Source #

Conjunction of a list of constraints.

Instances

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 :: a -> b -> Exp 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

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

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 :: [Match j k] -> j -> Exp 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

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