How to define constant heterogeneous streams in Haskell?

Question

I understand how to define both homogeneous and heterogeneous streams in 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)

How can we define a constant stream as a particular case of a heterogeneous stream? If I try to define a type family of streams of constant type, I get a "Reduction stack overflow" error. I imagine this has to do with the type checking algorithm not being lazy enough and trying to compute the whole Constant a stream of types.

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

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

Is there any way I can get around this problem and define constant heterogeneous streams? Is there any other similar construction I should be trying instead?

Answer 1

This is getting exactly at the distinction between inductive and co-inductive types, which we so like to ignore in Haskell. But you can't do that on the type level, because the compiler needs to make proofs in finite time.

So, what we need is to actually express the type-level stream in co-inductive fashion:

{-# 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)