Constructing heterogeneous lists

Using Coq
1

Hi.

I wanted to construct a heterogeneous list like

[[true; false]%vector;
 [true]%vector]%list

[Vector.t bool 2, Vector.t bool 3]

I was trying to follow Adam Chlipala’s CPDT book and defined an hlist as:

Inductive hlist {A : Type} {B : A -> Type} : list A -> Type :=
| HNil : hlist nil
| HCons : forall (x : A) (ls : list A), A -> hlist ls -> hlist (x :: ls).

The definition was executed without error.

But I couldn’t figure out how to construct the hlist.

I tried making an hlist like

(* Wanted to get [Vector.t bool 2; Vector.t bool 3] *)
Compute (HCons nat (fun (n:nat) => Vector.t bool n) [2;3]).
(*
The type of this term is a product while it is expected to be (list Set).
 *)

but ran into the error.

In fact, I couldn’t even figure out how to make the example given in the CPDT book work.

Example someValues : hlist (fun T : Set => T ) someTypes :=
  HCons 5 (HCons true HNil).
(*
The type of this term is a product while it is expected to be (list ?A).
 *)

I got error in the part of the anonymous function.

Couldn’t understand why someTypes is even needed here.

Is it that the elements of the hlist must belong to one of the types in someTypes?

Can’t we just make an hlist out of HCons with something like

Compute (HCons 5 (HCons true HNil)).

without resorting to use the Example command? Or is it to provide the value of B function?

What I thought was A is like a universal type for the elements in the list and B is a function which can be used to get the exact type for each of the elements in the hlist. Isn’t that so?

Any idea what I’m missing or not understanding here?

2

The list [Vector.t bool 2 ; Vector.t bool 3] is not an heterogenous list: it contains two terms of the same type, namely Set. You should just try and typecheck it as is.
You would need a heterogenous list if you wanted to have in the same list two vectors of different lengths, something like [ Vector.nil ; Vector.cons true 0 nil ].

3

Sorry. I meant an hlist like

Compute [[true; false]%vector;
         [true]%vector]%list.

I’ll edit the original post.

4

The issue you run into with the example from CPDT has to do with implicit arguments (in the book, the Implicit Arguments and Arguments commands are used to declare those). A working standalone version is the following:

Require Import Vector List.
Import VectorNotations.

Set Implicit Arguments.

Inductive hlist (A : Type) (B : A -> Type) : list A -> Type :=
| HNil : hlist B nil
| HCons : forall (x : A) (ls : list A), B x -> hlist B ls -> hlist B (x :: ls).

(* declare a bit more implicit arguments than the one automatically detected by Implicit Arguments *)
Arguments HNil {A B}.
Arguments HCons {A B x ls}.

Definition someTypes : list Set := nat :: bool :: nil.

Example someValues : hlist (fun T : Set => T) someTypes :=
  HCons 5 (HCons true HNil). (*now this works fine *)

As for the example you were looking for with vectors, the following works, along the very same ideas:

Definition someInt : list nat := 2 :: 1 :: nil.

Example someMoreValues : hlist (Vector.t bool) someInt :=
 HCons [true ; false] (HCons [true] HNil).

Regarding your questions: someType or someInt are needed in order to provide the list of types of your heterogenous list. More precisely, the list of types of an heterogeneous list hlist B someIndices is map B someIndices. Thus someType and someInt are used to help Coq give types to your heterogeneous list. You could also get rid of A and B and simply have a list of types, but this has drawbacks in term of formalization, as handling a list of types is often cumbersome. It is often easier to work with a list of nicer indices (and it is more general, as the example from CPDT shows).
Finally, Example is irrelevant, it is just a synonym for Definition (mostly used to give a clearer structure to the code).

5

Thanks! I had been stuck trying to understand this for some time now. I think I finally got it.