我了解如何在 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)
有什么方法可以解決這個問題并定義恒定的異構流？我應該嘗試其他類似的結構嗎？
uj5u.com熱心網友回復：
這正是歸納和共歸納型別之間的區別，我們很喜歡在 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)
轉載請註明出處，本文鏈接：https://www.uj5u.com/qukuanlian/365067.html