Stream: Coq users

Topic: Heterogenous list in coq


view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Oct 11 2021 at 09:04):

try Check @HCons.

view this post on Zulip Gaëtan Gilbert (Oct 11 2021 at 09:04):

or About HCons.

view this post on Zulip 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 Bto be the identity, so it basically removes the two parameters, and should be as expressive.

view this post on Zulip 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?

How can we use it?

view this post on Zulip 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 ?

view this post on Zulip Enrico Tassi (Oct 11 2021 at 09:40):

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

view this post on Zulip 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))).

view this post on Zulip 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'))).

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 11 2021 at 10:15):

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

view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Oct 11 2021 at 10:17):

And, oh, your hlist takes both A and B

view this post on Zulip Paolo Giarrusso (Oct 11 2021 at 10:19):

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

view this post on Zulip Paolo Giarrusso (Oct 11 2021 at 10:19):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Gaëtan Gilbert (Oct 11 2021 at 10:43):

(B : A -> Type}

mismatched parens

view this post on Zulip Julin S (Oct 11 2021 at 10:51):

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

view this post on Zulip 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…

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 11 2021 at 11:52):

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

view this post on Zulip Paolo Giarrusso (Oct 11 2021 at 11:52):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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)

view this post on Zulip 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: Oct 13 2024 at 01:02 UTC