Stream: Coq users

Topic: ✔ Indexing into an hlist


view this post on Zulip Julin S (Apr 09 2022 at 10:46):

I was making a heterogenous list (hlist) in the line of what's mentioned in here.

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

Arguments hnil {A B}.
Arguments hcons {A B x ls}.

This type checked all right.

And I was able to make hlists as well.

Example hls1 : hlist Set (fun x => x) [nat; bool] :=
  hcons 3 (hcons true hnil).

Then I tried making a function to index into the element of hlists and made an hidx function.

But that gave error.

Fixpoint hidx_helper {A : Type} (ls : list A) (idx : nat) : Type :=
  match idx, ls with
  | _, []%list => unit
  | O, (x::xs)%list => A
  | S n', (x::xs)%list => hidx_helper xs n'
  end.

Fixpoint hidx {A: Type} {B: A -> Type} {ls: list A}
  (idx : nat) (hls : hlist A B ls)
  : hidx_helper ls idx :=
  match idx, hls with
  | _, hnil _ _ => tt   (* --------ERROR here--------- *)
  | O, hcons _ _ _ _ x xs => x
  | S n', hcons _ _ _ _ x xs => hidx n' xs
  end.
(*
In environment
hidx : forall (A : Type) (B : A -> Type) (ls : list A) (idx : nat),
       hlist A B ls -> hidx_helper ls idx
A : Type
B : A -> Type
ls : list A
idx : nat
hls : hlist A B ls
The term "tt" has type "unit" while it is expected to have type
 "hidx_helper ?l@{l0:=[]} ?n@{i0:=0}".
*)

I guess the problem is that I can't let Coq know that hidx_helper [] 0 evaluates to unit?

Compute hidx_helper []%list 0.
(* = unit : Type *)

How can I set this right?

view this post on Zulip Julin S (Apr 09 2022 at 10:48):

And could there be a way where the hidx_helper needn't have been separately defined?
As it's used just to find the type of hidx?

view this post on Zulip Gaëtan Gilbert (Apr 09 2022 at 10:54):

I guess the problem is that I can't let Coq know that hidx_helper [] 0 evaluates to unit?

no, the problem is that it hasn't figured out that the return type is hidx_helper [] 0 so it can't evaluate it

try match idx , hls in hlist _ _ ls return hidx_helper ls idx with

view this post on Zulip Julin S (Apr 09 2022 at 11:25):

Thanks. That fixed the first branch of that match.

But the second is also having trouble that I couldn't figure out.

It says:

In environment
hidx : forall (A : Type) (B : A -> Type) (ls : list A) (idx : nat),
       hlist A B ls -> hidx_helper ls idx
A : Type
B : A -> Type
ls : list A
idx : nat
hls : hlist A B ls
a : A
l : list A
x : B a
xs : hlist A B l
The term "x" has type "B a" while it is expected to have type
 "hidx_helper (a :: l) 0".

view this post on Zulip Julin S (Apr 09 2022 at 11:25):

Could this be a similar problem?

view this post on Zulip Gaëtan Gilbert (Apr 09 2022 at 11:26):

the definition of the helper looks wrong to me, it uses only the length of the list but not its contents

view this post on Zulip Julin S (Apr 09 2022 at 11:49):

Yeah, I hadn't realized it.

view this post on Zulip Julin S (Apr 09 2022 at 11:50):

I changed it to:

Fixpoint hidx_helper (A : Type) (lslen idx : nat) : Type :=
  match idx, lslen with
  | _, O => unit
  | O, _ => A
  | S n', S lslen' => hidx_helper A lslen' n'
  (*| S n', (x::xs)%list => hidx_helper xs n' *)
  end.

Fixpoint hidx {A: Type} {B: A -> Type} {ls: list A}
  (idx : nat) (hls : hlist A B ls)
  : hidx_helper A (length ls) idx :=
  match idx, hls in (hlist _ _ ls) return
    (hidx_helper A (length ls) idx) with
  | _, hnil _ _ => tt
  | O, hcons _ _ _ _ x xs => x  (* Error here! *)
  | S n', hcons _ _ _ _ x xs => hidx n' xs
  end.

But got a similar error:

In environment
hidx : forall (A : Type) (B : A -> Type) (ls : list A) (idx : nat),
       hlist A B ls -> hidx_helper A (length ls) idx
A : Type
B : A -> Type
ls : list A
idx : nat
hls : hlist A B ls
a : A
l : list A
x : B a
xs : hlist A B l
The term "x" has type "B a" while it is expected to have type
 "hidx_helper A (length (a :: l)) 0".

view this post on Zulip Gaëtan Gilbert (Apr 09 2022 at 11:54):

it should be something like

Fixpoint hidx_helper {A : Type} (B:A->Type) (ls : list A) (idx : nat) {struct ls} : Type :=
  match idx, ls with
  | _, []%list => unit
  | O, (x::xs)%list => B x
  | S n', (x::xs)%list => hidx_helper B xs n'
  end.

view this post on Zulip Julin S (Apr 09 2022 at 12:02):

I used this helper like:

Fixpoint hidx {A: Type} {B: A -> Type} {ls: list A}
  (idx : nat) (hls : hlist A B ls)
  : hidx_helper (fun x=>Type) ls idx :=
  match idx, hls in (hlist _ _ ls) return
    (hidx_helper (fun x=>Type) ls idx) with
  | _, @hnil _ _ => tt
  | O, @hcons _ _ _ _ x xs => x
  | S n', @hcons _ _ _ _ x xs => hidx n' xs
  end.

But got error:

In environment
hidx : forall (A : Type) (B : A -> Type) (ls : list A) (idx : nat),
       hlist A B ls -> hidx_helper (fun _ : A => Type) ls idx
A : Type
B : A -> Type
ls : list A
idx : nat
hls : hlist A B ls
a : A
l : list A
x : B a
xs : hlist A B l
The term "x" has type "B a" while it is expected to have type
 "hidx_helper (fun _ : A => Type) (a :: l) 0".

I guess I'm using it wrong. How should it be used?

view this post on Zulip Gaëtan Gilbert (Apr 09 2022 at 12:02):

use B not fun x=>Type

view this post on Zulip Julin S (Apr 09 2022 at 12:16):

Thanks a lot. That works. Now let me spend some time understanding it. :smiley:

view this post on Zulip Notification Bot (Apr 09 2022 at 12:16):

Julin S has marked this topic as resolved.


Last updated: Feb 01 2023 at 13:03 UTC