Data.Vector.HFixed.TypeFuns

Type functions

Type proxy

Starting from version 7.8 GHC provides kind-polymorphic proxy data type. In those versions Data.Typeable.Proxy is reexported. For GHC 7.6 we have to define our own Proxy data type.

data Proxy t :: k -> *

A concrete, poly-kinded proxy type

Constructors

Proxy

Instances

Monad (Proxy *)

Functor (Proxy *)

Applicative (Proxy *)

Vector (Proxy *) a

Bounded (Proxy k s)

Enum (Proxy k s)

Eq (Proxy k s)

Ord (Proxy k s)

Read (Proxy k s)

Show (Proxy k s)

Ix (Proxy k s)

Generic (Proxy * t)

Monoid (Proxy k s)

NFData (Proxy * a)

Since: 1.4.0.0

type Dim (Proxy *) = Z

type Rep (Proxy k t) = D1 D1Proxy (C1 C1_0Proxy U1)

proxy :: t -> Proxy t

unproxy :: Proxy t -> t

Type functions

type family xs ++ ys :: [α]

Concaternation of type level lists.

Instances

type (++) k ([] k) ys = ys

type (++) k ((:) k x xs) ys = (:) k x ((++) k xs ys)

type family Len xs :: *

Length of type list expressed as type level naturals from fixed-vector.

Instances

type Len k ([] k) = Z

type Len k ((:) k x xs) = S (Len k xs)

type family Head xs :: α

Head of type list

Instances

type Head k ((:) k x xs) = x

type family HomList n a :: [α]

Homogeneous type list with length n and element of type a. It uses type level natural defined in fixed-vector.

Instances

type HomList k Z a = [] k

type HomList k (S n) a = (:) k a (HomList k n a)

type family Wrap f a :: [β]

Wrap every element of list into type constructor

Instances

type Wrap k k1 f ([] k1) = [] k

type Wrap k k1 f ((:) k1 x xs) = (:) k (f x) (Wrap k k1 f xs)