Opened 19 months ago

Last modified 2 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, vagarenko
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: #9269 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 (10)

comment:1 Changed 19 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 18 months ago by skeuchel

Cc: skeuchel added

comment:3 Changed 6 months ago by goldfire

Keywords: TypeInType added

comment:4 Changed 6 months ago by Iceland_jack

Cc: Iceland_jack added

TODO Add GHC to Wikipedia when implemented ;)

comment:5 Changed 5 months ago by RyanGlScott

Cc: RyanGlScott added

comment:6 in reply to:  description Changed 5 months 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 (edit: actually #9269, since it's a duplicate of that) since I would find that useful in its own right.

Last edited 3 months ago by RyanGlScott (previous) (diff)

comment:7 Changed 4 months ago by vagarenko

Cc: vagarenko added

comment:8 Changed 3 months ago by RyanGlScott

Blocked By: 9269 added

comment:9 Changed 2 weeks ago by andrewthad

@goldfire To my understanding, the priority of this ticket is getting induction recursion supported for GADTs. I'm unclear on how the "same recursive subgroup" error in the example you gave is related to the "same recursive subgroup" error that I run into with typeclasses. For example:

class Grounded v where
  type Rep (a :: v) :: RuntimeRep
  type Lifted (a :: v) :: Type
  type Unlifted (a :: v) :: TYPE (Rep a)
  ... some methods in here as well

This currently errors with:

sorted_int_type.hs:100:35: error:
    • Type constructor ‘Rep’ cannot be used here
        (it is defined and used in the same recursive group)
    • In the first argument of ‘TYPE’, namely ‘(Rep a)’
      In the kind ‘TYPE (Rep a)’
    |
100 |   type Unlifted (a :: v) :: TYPE (Rep a)
    |                                   ^^^

I have to split the class up:

class GroundSuper v where
  type Rep (a :: v) :: RuntimeRep
class GroundSuper v => Grounded v where
  type Lifted (a :: v) :: Type
  type Unlifted (a :: v) :: TYPE (Rep a)

It's not the worst thing ever, but it's kind of silly that what really is logically one typeclass needs to be split up into two typeclasses. It's not totally clear to me if this is really even the same issue as what you describe above or if fixing one automatically fixes the other, but it gives the same error message, which leads me to believe that they are somehow related.

comment:10 Changed 2 weeks ago by goldfire

comment:9 is certainly related, but still separate from the eventual goal of this ticket. I do think a fix for this ticket would fix comment:9, but comment:9 could also be fixed independently (and, I believe, more easily).

Note: See TracTickets for help on using tickets.