如何在Haskell中定义常数异构流？

Question

我了解如何在Haskell中定义同质和异质流。

-- Type-invariant streams.
data InvStream a where
   (:::) :: a -> InvStream a -> InvStream a

-- Heterogeneous Streams.
data HStream :: InvStream * -> * where
   HCons :: x -> HStream xs -> HStream (x '::: xs)

我们如何定义一个常量流作为异构流的一种特殊情况？如果我试图定义一个指定类型的流类型族，我会得到一个“减少堆栈溢出”错误。我想这与类型检查算法不够懒惰并尝试计算整个类型为Constant a的流有关。

type family Constant (a :: *) :: InvStream * where
  Constant a = a '::: Constant a

constantStream :: a -> HStream (Constant a)
constantStream x =  HCons x (constantStream x)

有没有什么方法可以规避这个问题并定义常量异构流？还有其他类似的结构我应该尝试吗？

- Mario Román

Answer 1

这涉及到归纳类型和协同归纳类型之间的区别，这是我们在 Haskell 中经常忽略的。但你不能在类型级别上做到这一点，因为编译器需要在有限时间内进行证明。

所以，我们需要实际上以协同归纳的方式表达类型级别的流：

{-# LANGUAGE GADTs, DataKinds, TypeFamilies #-}

import Data.Kind (Type)  -- The kind `*` is obsolete

class TypeStream (s :: Type) where
  type HeadS s :: Type
  type TailS s :: Type

data HStream s where
  HConsS :: HeadS s -> HStream (TailS s) -> HStream s

data Constant a

instance TypeStream (Constant a) where
  type HeadS (Constant a) = a
  type TailS (Constant a) = Constant a

constantStream :: a -> HStream (Constant a)
constantStream x = HConsS x (constantStream x)

- leftaroundabout