Module Generic_core_product

module Generic_core_product: sig .. end

Witness of product types.

'a product is a GADT whose type parameter is of the form:

t0 * (t1 * (t2 * ... * (tn * unit) ...))

The values are lists of witnesses 'a ty reflecting the components of the product.

module T: sig .. end

This module defines the product datatype and is meant to be open so that constructors can be used in pattern matching.

type 'a t = 'a T.product =

`\|`	`Nil : unit t`
`\|`	`Cons : 'a0 Ty.T.ty * 'b t -> ('a0 * 'b) t`

Synonym, so that Product.T.product might be refered to as Product.t

Product Constructors

Functions p0 to p6 build products from 0 to 6 types.

val p0 : unit t

val p1 : 'a Ty.T.ty -> ('a * unit) t

val p2 : 'a Ty.T.ty ->
       'b Ty.T.ty -> ('a * ('b * unit)) t

val p3 : 'a Ty.T.ty ->
       'b Ty.T.ty ->
       'c Ty.T.ty -> ('a * ('b * ('c * unit))) t

val p4 : 'a Ty.T.ty ->
       'b Ty.T.ty ->
       'c Ty.T.ty ->
       'd Ty.T.ty ->
       ('a * ('b * ('c * ('d * unit)))) t

val p5 : 'a Ty.T.ty ->
       'b Ty.T.ty ->
       'c Ty.T.ty ->
       'd Ty.T.ty ->
       'e Ty.T.ty ->
       ('a * ('b * ('c * ('d * ('e * unit))))) t

val p6 : 'a Ty.T.ty ->
       'b Ty.T.ty ->
       'c Ty.T.ty ->
       'd Ty.T.ty ->
       'e Ty.T.ty ->
       'f Ty.T.ty ->
       ('a * ('b * ('c * ('d * ('e * ('f * unit)))))) t

module Build: sig .. end

open Build to bring p0 to p6 in scope

Products as Lists

If we forget about their type index, values of type products are isomorphic to lists of types. Thus list functions can be specialised for products.

val fold : (Ty.ty' -> 'b -> 'b) -> 'b -> 'a t -> 'b

Corresponds to List.fold_right

val length : 'a t -> int

Corresponds to List.length

val list_of_prod : 'a t -> Ty.ty' list

Forgetting the type index 'a, we obtain a list of unindexed type codes Generic_core_ty.ty'

Dynamic Products

Just like Generic_core_ty.dyn is the union of all types, we define Generic_core_product.dynprod, the union of all product types. Each value must be tagged with the witness of its product type.

type 'a tuple = 'a t * 'a

A value tagged by the witness of its product type

type dynprod =

`\|`	`Dynprod : 'a tuple -> dynprod`

Union of all product types

val list_of_dynprod : dynprod -> Ty.dyn list

Dynamic products are isomorphic to lists of dynamic values

val dynprod_of_list : Ty.dyn list -> dynprod