How can we create a heterogenous list in coq?

I wanted a list like [1, true, "hello"].

This is what I tried:

```
Inductive hlist {A : Type} {B : A -> Type} : list A -> Type :=
| HNil : hlist []
| HCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
Compute (HNil). (* No error *)
Compute (@HCons true [] (fun x:bool => Type) (HNil)). (* The function is wrong? *)
```

Where am I going wrong?

try `Check @HCons.`

or About HCons.

I do not know what your context is, but do you really need both `A`

and `B`

? Couldn’t you instead do something like:

```
Inductive hlist : list Type -> Type :=
| HNil : hlist []
| HCons : forall (A : Type) (x : A) (ls : list Type), hlist ls -> hlist (A :: ls).
```

? This amounts to taking `A`

to be `Type`

and `B`

to be the identity, so it basically removes the two parameters, and should be as expressive.

@Meven Lennon-Bertrand In this definition, how can we construct `[1, true, "hello"]`

?

I (sort of blindly) tried doing

```
Compute HCons nat 3 HNil.
```

but that gave

```
The term "[nat]" has type "list Set" while it is expected to have type
"list Type" (universe inconsistency: Cannot enforce Set = hlist.u2).
```

forall (A : Type) (x : A) (ls : list Type), hlist ls -> hlist (A :: ls).

means that `HCons`

wants 4 arguments, right?

- A : Type
- x : A
- ls : list Type
- hlist ls

How can we use it?

I wanted a list like [1, true, "hello"].

Why don't you tag? eg `[ Int 1, Bool true, String "hello"]`

where `Inductive t := Int of int | Bool of bool | String of string`

?

You will hardly code anything useful with a list that possibly contains anything.

I rearranged the arguments a bit so that the list of types can be made implicit:

```
Inductive hlist : list Type -> Type :=
| HNil : hlist []
| HCons : forall (A : Type) (ls : list Type), A -> hlist ls -> hlist (A :: ls).
Arguments HCons {_ _}.
Compute (HCons 1 (HCons 1 (HCons true HNil))).
```

But indeed as Enrico reminds me, because type cannot be matched over, it will most likely be very difficult to do anything with this list. You might be better off using either his solution, or something like mine but using a reification of the types in the index list, something like:

```
Inductive code :=
| Bool : code
| Nat : code
| String : code.
Definition decode (c : code) : Type :=
match c with
| Bool => bool
| Nat => nat
| String => string
end.
Inductive hlist' : list code -> Type :=
| HNil' : hlist' []
| HCons' : forall (ls : list code) (c : code), decode c -> hlist' ls -> hlist' (c :: ls).
Arguments HCons' {_}.
Compute (HCons' Nat 1 (HCons' Bool true (HCons' String "hello"%string HNil'))).
```

Thanks could make an hlist like `Compute (HCons 1 (HCons "str"%string (HCons true HNil))).`

Would it be possible for us to modify this to have tuples?

I am trying to follow Adam Chlipala's CPDT book at http://adam.chlipala.net/cpdt/html/DataStruct.html (under the 'Heterogeneous list' section).

I tried to copy what they did with

```
Require Import List.
Require Import String.
Import List.ListNotations.
Require Import Vector.
Set Asymmetric Patterns.
Section hlist.
Variable A : Type.
Variable B : A -> Type.
Inductive hlist : list A -> Type :=
| HNil : hlist []
| HCons : forall (x : A) (ls : list A),
B x -> hlist ls -> hlist (x :: ls).
End hlist.
Arguments HNil {A B}.
Arguments HCons {A B x ls} _ _.
(*Arguments HCons [A B x ls].*)
Definition someTypes : list Set := nat :: bool :: [].
Example someValues : hlist (fun T : Set => T) someTypes :=
HCons 5 HNil.
```

but got error at the last line (at the anonymous function part) saying:

```
The type of this term is a product while it is expected to be a sort.
```

How could this be fixed?

the standard HList is indexed by a list of the types of the contents (https://hackage.haskell.org/package/HList-0.5.0.0/docs/Data-HList-HList.html), which addresses the problems about computing with it without matching on types

@Ju-sh just make someTypes a "list Type"?

@Paolo Giarrusso tried to give `someTypes`

as `list Type`

but then it gives error (because `nat`

and `bool`

are `Set`

?)

```
The term "[nat; bool]" has type "list Set" while it is expected to have type
"list Type" (universe inconsistency: Cannot enforce Set = hlist.50).
```

And, oh, your hlist takes both A and B

Hm; everything in Set is also in Type, so that error surprises me...

But the immediate error you got first is fixable with "hlist Set (your fun...)"

Paolo Giarrusso said:

Hm; everything in Set is also in Type, so that error surprises me...

This looks like an ugly issue of cumulativity not going through the `list`

type constructor

@Ju-sh how familiar are you with implicit arguments? your attempts in this thread suggest you might be used to working with "Set Implicit Arguments" (at the start of the file after the requires!), but you'll need to understand implicit args to make this work well. Feel free to ask questions.

Ju-sh said:

Would it be possible for us to modify this to have tuples?

Regarding tuples, have you looked at formalizing them using Record types?

@Paolo Giarrusso

I'm just getting started with coq, so usually don't use `Set Implicit Arguments`

although they seem to use it in the CPDT book.

It often confuses me.. So at first I tried to replicate the hlist definition without using any implicit arguments (as much as I could manage. Couldn't figure out how to make `B`

explicit) like:

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

(Edited to correct mismatched parenthesis)

`(B : A -> Type}`

mismatched parens

@Meven Lennon-Bertrand Not yet, I thought I better get hold of hlist first.

@Ju-sh I think `B`

is explicit there, but I don’t see how that code could possibly work? In any case you should probably drop `Set Asymmetric Patterns.`

, I’m not sure anybody uses it today…

if you don’t use implicits, I’d expect `HCons`

in your style to take 6 arguments: `A B x ls`

then the unnamed ones of types `B x`

and `hlist ls`

.

for that style, drop the `Arguments`

commands and all curly braces.

this is pretty unusable, but at least argument passing should become straightforward.

and personally, I’d recommend practising implicit arguments on something like defining your own `list`

, _before_ starting with `hlist`

Paolo Giarrusso said:

In any case you should probably drop

`Set Asymmetric Patterns.`

, I’m not sure anybody uses it today…

CompCert, MathComp, Flocq are using it. (And their users too, as they are `Global`

.) And presumably some other libraries too.

Ju-sh said:

Meven Lennon-Bertrand Not yet, I thought I better get hold of hlist first.

Sure! But depending on your background and what you want to do, they might actually be easier/more natural to use, so it might be worth checking it out (in the refman for instance).

@Guillaume Melquiond thanks for the correction. Still, @Ju-sh , Asymmetric Patterns complicates how constructor arguments work in pattern matching, since it forces one to omit certain constructor arguments even if they are not implicit, but only for pattern matches. (See https://coq.inria.fr/refman/language/extensions/match.html#coq:flag.Asymmetric-Patterns)

Personally, I rather tend to turn the parameters into implicit arguments, since that helps with construction as well.

Last updated: Jun 25 2024 at 15:02 UTC