haskell - Haskell 中的无限(最终周期性)HList

Question

假设我有一个无限的 Action 序列，每个 Action 都返回某种类型的结果。像这样的东西:

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 类型系统不支持的。但是我看不出最终周期性的 HList 有什么问题(即这样的类型序列会从某个点重复自身:[Bool, Int, Int, Sting, Int, Sting, Int, Sting ...] )。而且我还认为，如果我们有一些强规范化的方法来描述无限类型，或者有一些方法来提供无限类型相等性的证据，可以在有限的步骤中检查，那么应该可以对具有这种无限类型的程序进行类型检查。

有谁知道如何在 Haskell 中表示和使用这些类型？现在让我们从无限 finally-periodic hlist 开始，但如果有人知道如何将它泛化到更广泛的无限元组类别以及泛化限制所在，我也会很感激。

Answer 1

用这个很酷的技巧使 HList 无限且周期性!

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

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