GitLab

Now that we have -XTypeInType, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:

 mutual
   -- Codes for types.

   data U : Set where
     nat : U
     pi  : (a : U) → (El a → U) → U

   -- A function that interprets codes as actual types.

   El : U → Set
   El nat      = ℕ
   El (pi a b) = (x : El a) → El (b x)

Note that the U datatype and the El function depend on each other. But if you look more closely, the header for U does not depend on El; only the constructors of U depend on El. So if we typecheck U : Set first, then El : U → Set, then the constructors of U, then the equations of El, we're OK.

Translation into Haskell:

import Data.Kind

data family Sing (a :: k)  -- we still require singletons

data U :: Type where
  Nat :: U
  Pi  :: Sing (a :: U) -> (El a -> U) -> U

type family El (u :: U) :: Type where
  El 'Nat     = Int
  El (Pi a b) = forall (x :: El a). Sing x -> El (b x)

This currently errors with

    • Type constructor ‘U’ cannot be used here
        (it is defined and used in the same recursive group)
    • In the kind ‘U’

It needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a forall on the right-hand side of a type family. But that's not the issue at hand.)

I have some very sketchy notes on how we might do this here.

Trac metadata

Trac field	Value
Version	8.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture