Control.IndexT.Constructor

This module provides a way to constrain types to be data constructors, much like Control.IndexT.Tuple and Control.IndexT.Function.

It also provides type families for accessing the elements of those data constructors, both the constructors themselves and the parameters to them.

Note I haven't yet wrote code to generate many instances for these, so currently only constructors with up to two parameters is supported. Just nag me if your application needs more.

Documentation

type IndexC n i a = IndexCK Type n i a

IndexC i n (f a_0 a_1 .. a_(n-1))

the ith (zero based) parameter of the constructor with n parameters, i.e. a_i

This however only allows constructors with parameters of type :: Type, not of other kinds (see IndexCK)

type family IndexCK k (n :: Nat) (i :: Nat) a = (r :: k)

Just like 'IndexC' but has an additional kind parameter

Instances

type IndexCK k 1 0 (_ a)

type IndexCK k 1 0 (_ a) = a

type IndexCK k1 2 1 (_1 _ a)

type IndexCK k1 2 1 (_1 _ a) = a

type IndexCK k 2 0 (_ a _1)

type IndexCK k 2 0 (_ a _1) = a

These functions actually get the constructor, Unfortunately these are separate named functions instead of being indexed by n because they have different kinds, i.e. GetConstructor1 is * -> * whereas GetConstructor2 is * -> * -> *. If there's a better way of doing this let me know.

type family GetConstructor1 a where ...

Equations

GetConstructor1 (f _) = f

type family GetConstructor2 a where ...

Equations

GetConstructor2 (f _ _) = f

type family IsData (n :: Nat) a :: Constraint

Much like IsTuple and IsFunction, IsData m t asserts that t is a data constructor with n variables.

Instances

type IsData 1 a

type IsData 1 a

type IsData 2 a

type IsData 2 a