# GHC proposal: Lazy type families

**URL:** <https://discourse.haskell.org/t/ghc-proposal-lazy-type-families/6763>\
**Category:** Uncategorized\
**Created:** [June 30, 2023, 9:57am UTC](https://discourse.haskell.org/t/ghc-proposal-lazy-type-families/6763 "2023-06-30T09:57:52Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![Dani\_Rybe](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/dani_rybe/32/4253_2.png) [@Dani\_Rybe](https://discourse.haskell.org/u/Dani_Rybe)\
**Post date:** [June 30, 2023, 9:57am UTC](https://discourse.haskell.org/t/ghc-proposal-lazy-type-families/6763/1 "2023-06-30T09:57:52Z")

</div>

What if we had an extension that would make type family evaluation lazy? This would allow for infinite types such as in this example:

```haskell
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.

---

<div class="post-metadata">

**Author:** ![santiweight](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/santiweight/32/1187_2.png) [@santiweight](https://discourse.haskell.org/u/santiweight)\
**Post date:** [June 30, 2023, 12:18pm UTC](https://discourse.haskell.org/t/ghc-proposal-lazy-type-families/6763/2 "2023-06-30T12:18:49Z")

</div>

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).

---

<div class="post-metadata">

**Author:** ![adamgundry](https://avatars.discourse-cdn.com/v4/letter/a/34f0e0/32.png) [@adamgundry](https://discourse.haskell.org/u/adamgundry)\
**Post date:** [June 30, 2023, 8:30pm UTC](https://discourse.haskell.org/t/ghc-proposal-lazy-type-families/6763/3 "2023-06-30T20:30:14Z")

</div>

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:

> <https://github.com/ghc-proposals/ghc-proposals/pull/509>
>
> This proposal introduces a new way to use term-level functions at the type level…. 
> It saves the GHC from the necessity of having a lot of functions for built-in promoted types, it also allows users to make both complex and fast computations at the type level. 
> 
> \[Rendered\](https://github.com/Haskell-mouse/ghc-proposals/blob/type-functions/proposals/0000-type-functions.rst)

> **[\#18965: Make the rewriter work only at top-level · Issues · Glasgow Haskell...](https://gitlab.haskell.org/ghc/ghc/-/issues/18965)**
>
> In a recent conversation, @simonpj and I schemed about another way to simplify the solver.

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [July 1, 2023, 4:38am UTC](https://discourse.haskell.org/t/ghc-proposal-lazy-type-families/6763/4 "2023-07-01T04:38:20Z")

</div>

> [@Dani\_Rybe](#):
>
> ```haskell
> type family InfList a where
> InfList a = a : InfList a
> 
> ```

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)

```haskell
    data HetList where
         HetCons :: Show a => a -> HetList -> HetList
         -- HetNil :: HetList -- optional constructor
    deriving instance Show HetList

```

> [@adamgundry](#):
>
> Unfortunately the tricky bit is the constraint solver,

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.