Type.Cluss

Clusses

class In as a where

In as is a cluss, where as is a list of type patterns. Normally, as is concrete and does not contain any type variables, like In [Binary (->) (Show >|< This), Type String] a.

When a satisfies In as a, you can use the method proj :: AllOf as f -> f a.

Clusses call for some language extensions. Basically, this language pragma will do.

{-# LANGUAGE DataKinds, FlexibleContexts, TypeOperators #-}

Internally, "type pattern matching" is executed by Where, a closed type family, which cannot check if a type satisfies a constraint. If as has many type patterns that can match a, only the first one matches a.

Methods

proj :: AllOf as f -> f a

Instances

In' k (Where k as a) as as a => In k as a

Type Patterns

Type patterns are used in the type list (first parameter) of In. Each type pattern corresponds to the head of an instance declaration for a type class, namely, instance ... where.

data Type a

The empty type Type a is a type pattern. For example, the type pattern Type Int corresponds to instance C Int where ... (C is a type class). Note that the type variable a can be of any kind.

Instances

data AllOf' k ts ((:) * (Type k a) as) = And (f a) (AllOf' k ts as f)

data a <| p infixl 7

The empty type a <| p is a type pattern, where a is a type constructor, and p is a constraint function for the type variables for the constructor a. For example, the type pattern [] <| Show corresponds to instance (Show a) => C [a] where ... (C is a type class).

You can replace any of Unary, Binary, ..., Senary with <|, but you can sometimes save the effort of annotating kinds using Unary, Binary, ..., Senary instead of <|, especially when using PolyKinds extension, because kinds of parameters are restricted in Unary, Binary, ..., Senary.

Instances

data AllOf' k ts ((:) * (Senary k1 k2 k3 k4 k5 k6 k a p) as) = And6 (forall b c d e f' g. Modify6 k k k k k k (In k ts) p b c d e f' g => f (a b c d e f' g)) (AllOf' k ts as f)

data AllOf' k ts ((:) * (Quinary k1 k2 k3 k4 k5 k a p) as) = And5 (forall b c d e f'. Modify5 k k k k k (In k ts) p b c d e f' => f (a b c d e f')) (AllOf' k ts as f)

data AllOf' k ts ((:) * (Quaternary k1 k2 k3 k4 k a p) as) = And4 (forall b c d e. Modify4 k k k k (In k ts) p b c d e => f (a b c d e)) (AllOf' k ts as f)

data AllOf' k ts ((:) * (Ternary k1 k2 (k3 -> k) k3 a p) as) = And3 (forall b c d. Modify3 k k k (In k ts) p b c d => f (a b c d)) (AllOf' k ts as f)

data AllOf' k ts ((:) * (Binary k1 k2 k a p) as) = And2 (forall b c. Modify2 k k (In k ts) p b c => f (a b c)) (AllOf' k ts as f)

data AllOf' k ts ((:) * (Unary k1 k a p) as) = And1 (forall b. Modify k (In k ts) p b => f (a b)) (AllOf' k ts as f)

type Unary a p = a <| p

a <| p, with a being of the kind i -> k and p, i -> Constraint.

type Binary a p = a <| p

a <| p, with a being of the kind i -> i' -> k and p, i -> i' -> Constraint.

type Ternary a p = a <| p

a <| p, with a being of the kind i -> i' -> i'' -> k and p, i -> i' -> i'' -> Constraint.

type Quaternary a p = a <| p

a <| p, with a being of the kind i -> i' -> i'' -> i''' -> k and p, i -> i' -> i'' -> i''' -> Constraint.

type Quinary a p = a <| p

a <| p, with a being of the kind i -> i' -> i'' -> i''' -> i'''' -> k and p, i -> i' -> i'' -> i''' -> i'''' -> Constraint.

type Senary a p = a <| p

a <| p, with a being of the kind i -> i' -> i'' -> i''' -> i'''' -> i''''' -> k and p, i -> i' -> i'' -> i''' -> i'''' -> i''''' -> Constraint.

Instance Products

type AllOf as = AllOf' as as

AllOf as f is a tuple that contains values of the type f a, where a can be any type that satisfies In as a. Each value corresponds to each type pattern, and the values in AllOf as f must be in the same order as the type patterns in as. And, And1, And2, ..., And6 are used to combine the values and None must be added at the end. You have to use And for Type a, And1 for Unary a p, And2 for Binary a p, ..., And6 for Senary a p.

data family AllOf' ts as f

Instances

data AllOf' k ts ([] *) = None

data AllOf' k ts ((:) * (Senary k1 k2 k3 k4 k5 k6 k a p) as) = And6 (forall b c d e f' g. Modify6 k k k k k k (In k ts) p b c d e f' g => f (a b c d e f' g)) (AllOf' k ts as f)

data AllOf' k ts ((:) * (Quinary k1 k2 k3 k4 k5 k a p) as) = And5 (forall b c d e f'. Modify5 k k k k k (In k ts) p b c d e f' => f (a b c d e f')) (AllOf' k ts as f)

data AllOf' k ts ((:) * (Quaternary k1 k2 k3 k4 k a p) as) = And4 (forall b c d e. Modify4 k k k k (In k ts) p b c d e => f (a b c d e)) (AllOf' k ts as f)

data AllOf' k ts ((:) * (Ternary k1 k2 (k3 -> k) k3 a p) as) = And3 (forall b c d. Modify3 k k k (In k ts) p b c d => f (a b c d)) (AllOf' k ts as f)

data AllOf' k ts ((:) * (Binary k1 k2 k a p) as) = And2 (forall b c. Modify2 k k (In k ts) p b c => f (a b c)) (AllOf' k ts as f)

data AllOf' k ts ((:) * (Unary k1 k a p) as) = And1 (forall b. Modify k (In k ts) p b => f (a b)) (AllOf' k ts as f)

data AllOf' k ts ((:) * (Type k a) as) = And (f a) (AllOf' k ts as f)

Constraint Combinators

Constraint combinators are used in the second parameter of <|, Unary, Binary, ..., Senary. Note that each combinator is kind-polymorphic.

Basic Combinators

class (True ~ False) => This a

This creates a recursion. In other words, This will work as In as itself when used in the type list (first parameter) as of In, combined with Type, <|, Unary, Binary, ..., Senary, >+<, >++<, ..., >++++++<, >|<, >||<, ..., >|||||<.

Note that This won't be expanded into In as if the condition described above is not satisfied. Internally, the expansion is executed by Modify, Modify2, ..., Modify6.

The instance of This itself can't be created since the context True~False will never be satisfied.

There is no predetermined limit of recursion depth, but GHC has a fixed-depth recursion stack for safety, so you may need to increase the stack depth with -fcontext-stack=N.

class Pure a

Pure a is equivalent to the empty constraint ().

Pure a == ()

Instances

Pure k a

type Is a b = a ~ b

(Is a) b == (a ~ b)

Combinators for Overlaying Contraints

class (p a, q a) => (p >+< q) a infixl 9

(p >+< q) a == (p a, q a)

Instances

(p a, q a) => (>+<) k p q a

class (p a b, q a b) => (p >++< q) a b infixl 9

(p >++< q) a b == (p a b, q a b)

Instances

(p a b, q a b) => (>++<) k k p q a b

class (p a b c, q a b c) => (p >+++< q) a b c infixl 9

(p >+++< q) a b c == (p a b c, q a b c)

Instances

(p a b c, q a b c) => (>+++<) k k k p q a b c

class (p a b c d, q a b c d) => (p >++++< q) a b c d infixl 9

(p >++++< q) a b c d == (p a b c d, q a b c d)

Instances

(p a b c d, q a b c d) => (>++++<) k k k k p q a b c d

class (p a b c d e, q a b c d e) => (p >+++++< q) a b c d e infixl 9

(p >+++++< q) a b c d e == (p a b c d e, q a b c d e)

Instances

(p a b c d e, q a b c d e) => (>+++++<) k k k k k p q a b c d e

class (p a b c d e f, q a b c d e f) => (p >++++++< q) a b c d e f infixl 9

(p >++++++< q) a b c d e f == (p a b c d e f, q a b c d e f)

Instances

(p a b c d e f, q a b c d e f) => (>++++++<) k k k k k k p q a b c d e f

Combinators for Bonding Contraints

class (p a, q b) => (p >|< q) a b infixl 8

(p >|< q) a b == (p a, q b)

Instances

(p a, q b) => (>|<) k k p q a b

class (p a b, q c) => (p >||< q) a b c infixl 8

(p >||< q) a b c == (p a b, q c)

Instances

(p a b, q c) => (>||<) k k k p q a b c

class (p a b c, q d) => (p >|||< q) a b c d infixl 8

(p >|||< q) a b c d == (p a b c, q d)

Instances

(p a b c, q d) => (>|||<) k k k k p q a b c d

class (p a b c d, q e) => (p >||||< q) a b c d e infixl 8

(p >||||< q) a b c d e == (p a b c d, q e)

Instances

(p a b c d, q e) => (>||||<) k k k k k p q a b c d e

class (p a b c d e, q f) => (p >|||||< q) a b c d e f infixl 8

(p >|||||< q) a b c d e f == (p a b c d e, q f)

Instances

(p a b c d e, q f) => (>|||||<) k k k k k k p q a b c d e f

Helpers

Helpers for Identical Constructors

type AllOfI as = AllOfI' as as

type AllOfI' ts as = AllOf' ts as Id

andI :: a -> AllOfI' ts as -> AllOfI' ts (Type a : as) infixr 0

andI1 :: (forall b. Modify (In ts) p b => a b) -> AllOfI' ts as -> AllOfI' ts ((a <| p) : as) infixr 0

andI2 :: (forall b c. Modify2 (In ts) p b c => a b c) -> AllOfI' ts as -> AllOfI' ts ((a <| p) : as) infixr 0

andI3 :: (forall b c d. Modify3 (In ts) p b c d => a b c d) -> AllOfI' ts as -> AllOfI' ts ((a <| p) : as) infixr 0

andI4 :: (forall b c d e. Modify4 (In ts) p b c d e => a b c d e) -> AllOfI' ts as -> AllOfI' ts ((a <| p) : as) infixr 0

andI5 :: (forall b c d e f. Modify5 (In ts) p b c d e f => a b c d e f) -> AllOfI' ts as -> AllOfI' ts ((a <| p) : as) infixr 0

andI6 :: (forall b c d e f g. Modify6 (In ts) p b c d e f g => a b c d e f g) -> AllOfI' ts as -> AllOfI' ts ((a <| p) : as) infixr 0

noneI :: AllOfI' ts []

projI :: In as a => AllOfI as -> a

Helpers for Function Constructors

type AllOfF as t = AllOfF' as as t

type AllOfF' ts as t = AllOf' ts as (Func t)

andF :: (a -> t) -> AllOfF' ts as t -> AllOfF' ts (Type a : as) t infixr 0

andF1 :: (forall b. Modify (In ts) p b => a b -> t) -> AllOfF' ts as t -> AllOfF' ts ((a <| p) : as) t infixr 0

andF2 :: (forall b c. Modify2 (In ts) p b c => a b c -> t) -> AllOfF' ts as t -> AllOfF' ts ((a <| p) : as) t infixr 0

andF3 :: (forall b c d. Modify3 (In ts) p b c d => a b c d -> t) -> AllOfF' ts as t -> AllOfF' ts ((a <| p) : as) t infixr 0

andF4 :: (forall b c d e. Modify4 (In ts) p b c d e => a b c d e -> t) -> AllOfF' ts as t -> AllOfF' ts ((a <| p) : as) t infixr 0

andF5 :: (forall b c d e f. Modify5 (In ts) p b c d e f => a b c d e f -> t) -> AllOfF' ts as t -> AllOfF' ts ((a <| p) : as) t infixr 0

andF6 :: (forall b c d e f g. Modify6 (In ts) p b c d e f g => a b c d e f g -> t) -> AllOfF' ts as t -> AllOfF' ts ((a <| p) : as) t infixr 0

noneF :: AllOfF' ts [] t

projF :: In as a => AllOfF as t -> a -> t

Examples

Example1: Hello

Let's begin with a basic example.

type Hellos = [
    Type String,
    Type Int,
    Type Double,
    Unary [] Show,
    Quaternary (,,,) (This >|< This >||< This >|||< This)]
hello :: In Hellos a => a -> String
hello = projF (
    (\s -> "hello, " ++ s) `andF`
    (\n -> "Mr. " ++ show n) `andF`
    (\x -> show (x / 2) ++ " times two") `andF`
    (\xs -> concatMap ((++", ") . show) xs ++ "period") `andF1`
    (\(x,y,z,w) ->
        hello x ++ " and " ++ hello y ++ " and " ++
        hello z ++ " and " ++ hello w) `andF4`
    noneF :: AllOfF Hellos String)

main = putStrLn $
    hello ("world", 42 :: Int, 3.14 :: Double, [True, False])

This is the result.

hello, world and Mr. 42 and 1.57 times two and True, False, period

Example2: Printf

With a recursive cluss, you can easily make a function that can take a variable number of arguments. The function below is a simplified C-style printf.

type Printfs = [Binary (->) (Show >|< This), Type String]
printf :: In Printfs a => String -> a
printf s = projI (
    (\x -> printf (go s (show x))) `andI2`
    s `andI`
    noneI :: AllOfI Printfs)
  where
    go ('@' : cs) t = t ++ cs
    go (c : cs) t = c : go cs t
    go [] t = error "there is no '@' any more!"

main = putStrLn $
    printf "@ good @ and @" 12 "men" True

This is the result.

12 good "men" and True

Example3: Monad

Here is a more complex example. When the type of a "cluss method" is complex, you generally have to create newtypes (like Bind and Return below).

type Monads = [Type [], Unary (->) Pure, Unary (,) Monoid, Unary Wrap This]
newtype Wrap m a = Wrap {unWrap :: m a}
newtype Bind a b m = Bind {unBind :: m a -> (a -> m b) -> m b}
newtype Return a m = Return {unReturn :: a -> m a}
bind :: In Monads m => m a -> (a -> m b) -> m b
bind = unBind $ proj (
    Bind (\m k -> concatMap k m) `And`
    Bind (\m k e -> k (m e) e) `And1`
    Bind (\(a,x) k -> let (a',x') = k x in (a<>a',x')) `And1`
    Bind (\m k -> Wrap (unWrap m `bind` (unWrap . k))) `And1`
    None :: AllOf Monads (Bind a b))
return' :: In Monads m => a -> m a
return' = unReturn $ proj (
    Return (: []) `And`
    Return const `And1`
    Return ((,) mempty) `And1`
    Return (Wrap . return') `And1`
    None :: AllOf Monads (Return a))
infixl 1 `bind`

main = print $
    return' 1 `bind` replicate 3 `bind` (\n -> [n .. n+4])

This is the result.

[1,2,3,4,5,1,2,3,4,5,1,2,3,4,5]