Opened 2 years ago
Last modified 6 months 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 2 years ago by
Cc: | alexvieth added |
---|
comment:2 Changed 2 years ago by
Cc: | skeuchel added |
---|
comment:3 Changed 12 months ago by
Keywords: | TypeInType added |
---|
comment:4 Changed 12 months ago by
Cc: | Iceland_jack added |
---|
TODO Add GHC to Wikipedia when implemented ;)
comment:5 Changed 11 months ago by
Cc: | RyanGlScott added |
---|
comment:6 Changed 11 months ago by
Related Tickets: | → #13901 |
---|
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.
comment:7 Changed 10 months ago by
Cc: | vagarenko added |
---|
comment:8 Changed 9 months ago by
Blocked By: | 9269 added |
---|
comment:9 Changed 6 months ago by
@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.
(@goldfire mentioned in ticket:11348#comment:17 that @alexvieth might be interested in working on this ticket, so I'm CC-ing him here)