Opened 15 months ago

Last modified 3 weeks ago

#11962 new feature request

Support induction recursion

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.1
Keywords: TypeInType Cc: alexvieth, skeuchel, Iceland_jack, RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #13901 Differential Rev(s):
Wiki Page:

Description

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.

Change History (6)

comment:1 Changed 14 months ago by thomie

Cc: alexvieth added

(@goldfire mentioned in ticket:11348#comment:17 that @alexvieth might be interested in working on this ticket, so I'm CC-ing him here)

comment:2 Changed 14 months ago by skeuchel

Cc: skeuchel added

comment:3 Changed 7 weeks ago by goldfire

Keywords: TypeInType added

comment:4 Changed 7 weeks ago by Iceland_jack

Cc: Iceland_jack added

TODO Add GHC to Wikipedia when implemented ;)

comment:5 Changed 5 weeks ago by RyanGlScott

Cc: RyanGlScott added

comment:6 in reply to:  description Changed 3 weeks ago by RyanGlScott

Replying to goldfire:

(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'm tracking this issue separately at #13901, since I would find that useful in its own right.

Note: See TracTickets for help on using tickets.