9

我了解如何在 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)

有什么办法可以解决这个问题并定义恒定的异构流？我应该尝试其他类似的结构吗？

4

1 回答 1

9

这正是归纳和共归纳类型之间的区别，我们喜欢在 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)
于 2021-11-23T15:55:12.977 回答