2

假设我有一个无限的动作序列，每个动作都返回某种类型的结果。就像是：

newtype Stream a = Stream (IO (a, Stream a))

但随着a时间的推移而变化。我想强烈输入这个序列。对于任意无限类型序列和幼稚的方法，这显然没有意义，例如：

data HStream :: [u] -> * where Cons :: Proxy x -> HStream xs -> HStream (x ': xs)

infiniteInt = Cons (Proxy :: Proxy Int) infiniteInt

将导致无限类型，这是 Haskell 的类型系统不支持的。但是我认为final-periodic HLists 没有任何问题（即，这种类型的序列会从某个点重复自身：）[Bool, Int, Int, Sting, Int, Sting, Int, Sting ... ]。而且我还认为，如果我们有某种强烈的规范化方式来描述无限类型或某种方式来提供可以在有限步数中检查的无限类型相等性的证据，那么应该可以对具有这种无限类型的程序进行类型检查。

有谁知道如何在 Haskell 中表示和使用这些类型？现在让我们从无限最终周期 hlist 开始，但如果有人知道如何将它推广到更广泛的无限 tupes 类以及泛化限制在哪里，我将不胜感激。

4

2 回答 2

5

用这个 One Cool Trick让HLists 无限且周期性！

当您将元素添加到周期性异构流中时，不要扩展索引它的类型列表。旋转它。

type family Append x xs where
    Append x '[] = '[x]
    Append x (y ': xs) = y ': Append x xs

infixr 5 :::
data HStream as where
    (:::) :: { headHS :: a, tailHS :: HStream (Append a as) } -> HStream (a ': as)

myHStream :: HStream '[Char, Bool, Int]
myHStream = 'c' ::: True ::: 3 ::: 'x' ::: False ::: -5 ::: myHStream
于 2016-05-04T18:10:55.180 回答
1

一个通用的选项是从HList编码所有元素的类型的 切换到类型对齐的列表（或更一般地说，类型对齐的序列），它只确保沿有效路径的转换。

data TAList c x z where
  Nil :: TAList c x x
  Cons :: c x y -> TAList c y z -> TAList c x z

因此，您可以谨慎地使用可能性大的 GADTc和您选择的x和对您的转换进行编码z。无限类型对齐列表没有问题，因为它们的最终类型参数是多态的。

您可能可以使用 McBride 风格的索引方案而不是 Atkey 来获得更大的灵活性，但代价是更加复杂。

于 2016-05-05T01:23:37.227 回答