What if we had an extension that would make type family evaluation lazy? This would allow for infinite types such as in this example:
type family InfList a where
InfList a = a : InfList a
data Pipe is os where
Need :: (i -> Pipe is os) -> Pipe (i : is) os
Ready :: o -> Pipe is os -> Pipe is (o : os)
Done :: Pipe '[] '[]
outlet :: Pipe '[] (InfList a)
outlet a = Ready a (outlet a)
In the above example, when evaluating the type of outlet the compiler tries to eagerly evaluate InfList a and hits the reduction stack overflow. If it were to only evaluate InfList a to a : InfList a then it would be able to type check.
I’m not on the inside here. But I know that Type Family evaluation is a sore spot in general.
I forget: can types include type equalities in GHC? If so, then you need to evaluate types in order to know where they are well-constructed (and thus the program is well constructed).
This is perfectly reasonable from a GHC Core (System FC) perspective, which makes no assumptions about type family termination. Unfortunately the tricky bit is the constraint solver, which has to solve a wide range of equality constraints involving type families.
The current design makes absolutely no attempt to give them any kind of sensible operational semantics, because it is coming from a logical rather than operational perspective. Type family reduction is neither strict nor lazy as such; instead, GHC reduces essentially arbitrary redexes (and exploits given equality constraints whenever it feels like it) to try to make the program typecheck. In addition, closed type families permit reduction steps that make sense if reading them as equations, but are difficult to interpret operationally (e.g. they don’t map nicely onto case-splitting trees).
All this is good for accepting lots of programs without too many type annotations or explicit appeals to equality constraints. But it is rather bad for performance of type family reduction, and makes it difficult to translate programs that rely on term-level laziness into their type-level equivalents.
Given backwards compatibility constraints, I suspect the most feasible way forward would be to introduce a new flavour of type families with a clearly defined operational semantics (ideally compatible with lazy evaluation in term-level Haskell) but potentially less automated equational reasoning in the constraint solver. It’s quite a technically tricky area, however, so I’m not sure we’re likely to see progress any time soon.
A couple of related links that might be of interest:
Welcome @Dani_Rybe. Emm I’m not getting the ‘why’ in your use case:
Are the list elements all the same type? Then why not use an ordinary infinite/lazy list :: [a]?
Or if the elements are various types: without a constraint somewhere, you can’t do anything useful with the elements except pass them along the Pipe(?)
Would a GADT fit the bill better? (With a Show instance, for example)
data HetList where
HetCons :: Show a => a -> HetList -> HetList
-- HetNil :: HetList -- optional constructor
deriving instance Show HetList
Yeah, as Adam says, if you want your list type to be passed/consumed elsewhere in the program, the compiler will want to infer/solve for a tractable (probably finite) type.
