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

标签 haskell types dependent-type hlist

假设我有一个无限的 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 开始,但如果有人知道如何将它泛化到更广泛的无限元组类别以及泛化限制所在,我也会很感激。

最佳答案

用这个很酷的技巧使 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

关于haskell - Haskell 中的无限(最终周期性)HList,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/37034545/

相关文章:

haskell - Haskell 编译器如何决定是在堆上分配还是在栈上分配?

haskell - 在 monad 转换器中使用类型同义词

multithreading - 为什么 GHC 线程重量极轻?

haskell - 具有重载数字和字符串文字的类型类多态性

c++ - 使用 CRTP 的模板中的继承类型

haskell - Agda 类型检查和交换性/+ 的关联性

python 3 typing varadic "apply"样式定义

struct - 如何向具有同类类型的结构/元组添加索引支持?

scala - scala 不明确支持依赖类型的任何原因?

c++ - 嵌套两次的 sizeof 可以是依赖表达式吗?