异构列表上的此类型错误是什么意思？

Question

我有一个异构列表和一个函数

type ('ls,'tl) hlist =
  | Nil : ('a,'a) hlist
  | Cons: 'a * ('l, 't) hlist -> ('a -> 'l, 't) hlist

let rec headlist l = 
  match l with
  | Cons (h, t) -> Cons (head h, headlist t)
  | Nil -> Nil

并且想要遍历不同类型的hlist中的list，并建立每个列表的首部列表。这个想法是这样的：

headlist Cons( [1,2,3], Cons( ['a','b'], Cons( [true,false], Nil ))) 
= Cons( 1, Cons( 'a', Cons( true, Nil)))

但是，我遇到类型错误。

Error: This expression has type ('a, 'b list -> 'a) hlist
       but an expression was expected of type
         ('b list -> 'a, 'b list -> 'a) hlist
       The type variable 'a occurs inside 'b list -> 'a

我不了解类型错误。在说什么我是否在尝试做一些不可能的事情？

Answer 1

我认为没有一种类型可以描述您想要的功能。您想说输入是一个hlist，所有异构类型都是列表。我看不出有这种说法，这表明我无法拥有这样的功能。

但是，我错了很多次，GADT是我特别不稳定的事情。