## Stream: Coq users

### Topic: Heterogenous list in coq

#### Julin S (Oct 11 2021 at 08:48):

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?

#### Gaëtan Gilbert (Oct 11 2021 at 09:04):

try `Check @HCons.`

#### Meven Lennon-Bertrand (Oct 11 2021 at 09:13):

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.

#### Julin S (Oct 11 2021 at 09:35):

@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?

#### Enrico Tassi (Oct 11 2021 at 09:39):

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` ?

#### Enrico Tassi (Oct 11 2021 at 09:40):

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

#### Meven Lennon-Bertrand (Oct 11 2021 at 09:41):

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))).
``````

#### Meven Lennon-Bertrand (Oct 11 2021 at 09:57):

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'))).
``````

#### Julin S (Oct 11 2021 at 10:14):

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?

#### Paolo Giarrusso (Oct 11 2021 at 10:14):

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

#### Paolo Giarrusso (Oct 11 2021 at 10:15):

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

#### Julin S (Oct 11 2021 at 10:17):

@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).
``````

#### Paolo Giarrusso (Oct 11 2021 at 10:17):

And, oh, your hlist takes both A and B

#### Paolo Giarrusso (Oct 11 2021 at 10:19):

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

#### Paolo Giarrusso (Oct 11 2021 at 10:19):

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

#### Meven Lennon-Bertrand (Oct 11 2021 at 10:20):

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

#### Paolo Giarrusso (Oct 11 2021 at 10:22):

@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.

#### Meven Lennon-Bertrand (Oct 11 2021 at 10:22):

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?

#### Julin S (Oct 11 2021 at 10:38):

@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)

#### Gaëtan Gilbert (Oct 11 2021 at 10:43):

`(B : A -> Type}`

mismatched parens

#### Julin S (Oct 11 2021 at 10:51):

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

#### Paolo Giarrusso (Oct 11 2021 at 11:49):

@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…

#### Paolo Giarrusso (Oct 11 2021 at 11:51):

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`.

#### Paolo Giarrusso (Oct 11 2021 at 11:52):

for that style, drop the `Arguments` commands and all curly braces.

#### Paolo Giarrusso (Oct 11 2021 at 11:52):

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

#### Paolo Giarrusso (Oct 11 2021 at 11:55):

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

#### Guillaume Melquiond (Oct 11 2021 at 11:56):

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.

#### Meven Lennon-Bertrand (Oct 11 2021 at 11:58):

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).

#### Paolo Giarrusso (Oct 12 2021 at 05:15):

@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)

#### Paolo Giarrusso (Oct 12 2021 at 05:20):

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