时间戳

首页 > 解决方案 > 从普通列表创建索引链接列表

haskell - 从普通列表创建索引链接列表

问题描述

我目前正在使用索引链表。基本数据类型由下式给出

data LList (n :: Nat) (a :: Type) where
  Nil  ::LList 0 a
  (:@) ::a -> LList n a -> LList (n + 1) a

我想知道是否可以定义从[]to的映射LList？

返回类型取决于运行时信息，因为列表的长度当然在编译时不可用。

fromList :: ? => [a] => LList ? a
fromList = undefined

游乐场的完整源代码可在此处获得。

标签： haskelldependent-typetype-level-computation

解决方案

是的，只需使用存在主义。这将列表的长度和列表本身包装成一对，它不会在类型中显示其长度。

data SomeLList a = forall n. SomeLList (LList n a)

这表示 aSomeLList a包含一个形式为 的项SomeLList @(n :: Nat) (_ :: LList n a)。这种类型实际上等价于[]（除了一个额外的底部并且没有无穷大）

fromList :: [a] -> SomeLList a
fromList [] = Nil
fromList (x : xs) | SomeList xs' <- fromList xs = SomeList (x :@ xs)

您可以通过匹配从配对中获取类型：

something :: [a] -> ()
something xs
  | SomeList xs' <- fromList xs
  = -- here, xs' :: SomeList n xs, where n :: Nat is a new type (invisibly) extracted from the match
    -- currently, we don't know anything about n except its type, but we could e.g. match on xs', which is a GADT and could tell us about n
    ()

推荐阅读