Verifying type families for termination and correctness

Learn
1

Hi,

Powerful Haskell type system helps to catch errors, but as the number of type functions and their sizes grows I anticipate the opposite effect and I would like to have a way to verify them.

Is there a tool or technique capable of checking that type family terminates under certain condition? LiquidHaskell and extraction from Agda are the first things that pop up in my head, but they can’t do that, do they?

2

Hello! I don’t think LiquidHaskell can check termination of type families. If you wanted to do the termination checks with SMT solvers, then changing LiquidHaskell could be worth considering, or using liquid-fixpoint.

I don’t know about Agda. I guess that any translation from and to dependently typed languages could play similar roles.

Other alternatives would be to implement termination checks in a plugin, or in GHC, or in a standalone tool. :thinking:

Picking approaches would require collecting and classifying examples of type families that need to be supported.

3

Interesting question! I’m having difficulties to define what termination even means for type families. Let’s try to work out what is needed to solve this.
Please correct me if you think any of the following is not accurate.

In first approximation, a type family is a function f :: Type -> ... -> Type. Let us forget that we are actually dealing with types and abstract to f :: t -> ... -> t.

Next question is, what primitives are available to build f?

  • We certainly have recursion, otherwise the question of termination would be trivial. But it is not a full untyped or simply-typed lambda calculus, because there is no currying or partial application in type families, right? At least GHC currently does not support this.
  • There is no type of type families. In other words, no higher-rank families. data FamilyKind = Kind | Kind :->: FamilyKind Note: No FamilyKind on the LHS of the arrow.
  • We have a context of known type names in scope, which we can regard as elements of t. Moreover, type family declarations can be mutually recursive.
  • We have pattern matching on values of t, at least to some extent. We can certainly match on known primitive types names like Int.
  • Type families are partial in general. Would you consider a properly partial type family as terminating?

So we have something like a simply-typed lambda calculus, with recursion, (partial) pattern matching and variables, but only application, no lambda abstraction. The Dec type in Template Haskell might give hints where I have over-simplified.

Finally, in our hypothetical universe of type families t -> ... -> t, what counts as termination? I suppose we need a reduction relation similarly to what we have in lambda calculus and say a type family terminates when variable-free terms have a normal form.

All in all, when you ask for type family termination tools, you should look for tools that can prove normalization in lambda calculi. I don’t know whether the absence of lambda abstraction makes this problem any easier.

4

A naive termination checker like Liquid Haskell has seems relatively straightforward: check if at least one argument (uniformly) shrinks every recursive call (can be extended to cover more cases). There are at least two complications: Type :: Type and data types that are not strictly positive. Perhaps those are also not that hard to approximate?

5

Dependent haskell is being worked on. After this , i think it would be very interesting to see whether termination checking for runtime and type level code ( type families ) , could performed. This would make haskell more in line with idris2, which has dependent types ( but not yet soundness, girards paradox and other problems are still at large, but devs say this could be fixed without upending the language )

6

is termination checking on the DH roadmap?

7

Termination checking falls outside the scope of DH, but it’d be a great post-DH addition.