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 family IndexC (n :: Nat) (i :: Nat) (a :: k1) = (r :: k2)

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

Instances

type IndexC k2 k1 1 0 (_ a)

type IndexC k2 k1 1 0 (_ a) = a

type IndexC k2 k1 2 1 (_1 _ a)

type IndexC k2 k1 2 1 (_1 _ a) = a

type IndexC k2 k1 2 0 (_ a _1)

type IndexC k2 k1 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