时间戳

首页 > 解决方案 > 异构列表上的这种类型错误是什么意思？

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

问题描述

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

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

我不明白类型错误。它在说什么？我在尝试做一些不可能的事情吗？

标签： ocamlgadt

解决方案

您的问题始于无法为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变得简单：

let rec map_head:
  type l hl. (l, hl) Hlist_of_nonempty_hlist.t -> hl Hlist.t
  = function
  | [] -> []
  | (a::_) :: q -> a :: map_head q

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

推荐阅读