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

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的lists ，并构建每个列表的头部的列表。这个想法是这样的：

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

您的问题始于这样一个事实，即无法为headlist您想到的函数编写类型。由于通常需要明确地编写操作 GATD 的函数类型，因此开始编写这种类型以检查是否可以编写该类型是一种很好的做法；并且仅在可以省略显式类型注释的极少数情况下才将其删除。

这里问题的根源在于异构列表比普通列表更加严格。特别是，根据对此类列表所需的操作，经常需要定制专门的异构列表类型。例如，对于经典的异构列表：

type void = |
module Hlist = struct
  type 'a t =
    | []: void t
    | (::): 'a * 'l t -> ('a -> 'l) t

  let head(x::_) = x
  let rec length: type a. a t -> int = function
    | [] -> 0
    | a :: q -> 1 + length q 
end

不可能表达条件：异构列表的所有元素都是异构列表，其中至少有一个元素本身。但是，可以定义另一个强制执行此条件的列表类型：

module Hlist_of_nonempty_hlist_0 = struct
  type 'a t =
    | []: void t
    | (::): (('h -> 'more) as 'a) Hlist.t * 'l t -> ('a -> 'l) t
end

使用这种新的列表类型，我可以计算所有嵌套列表的长度：

let rec map_length: type a. a Hlist_of_nonempty_hlist_0 t -> int list = function
 | [] -> []
 | a :: q -> Hlist.length a :: map_length q 

但是，我仍然不能适用head于所有元素，因为头部的类型不容易访问。一种选择是将这些类型直接存储在以下类型中Hlist_of_nonempty_hlist：

module Hlist_of_nonempty_hlist = struct
  type ('a,'b) t =
    | []: (void,void) t
    | (::):
       (('h -> 'more) as 'a) Hlist.t * ('l,'hl) t
       -> ('a -> 'l, 'h -> 'hl) t
end

使用这种特殊的异构列表类型，编写类型map_head变得很简单：

type void = |
module Hlist = struct
  type 'a t =
    | []: void t
    | (::): 'a * 'l t -> ('a -> 'l) t

  let head(x::_) = x
  let rec length: type a. a t -> int = function
    | [] -> 0
    | a :: q -> 1 + length q 
end

但这是对一个功能的类型进行的大量设计工作。更进一步，尝试在异构列表上编写任何通用函数通常需要大量多态记录和函子。