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?
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: Oct 13 2024 at 01:02 UTC