Opened 17 months ago
Last modified 5 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 (8)
comment:1 Changed 16 months ago by
Cc: | alexvieth added |
---|
comment:2 Changed 16 months ago by
Cc: | skeuchel added |
---|
comment:3 Changed 4 months ago by
Keywords: | TypeInType added |
---|
comment:4 Changed 4 months ago by
Cc: | Iceland_jack added |
---|
TODO Add GHC to Wikipedia when implemented ;)
comment:5 Changed 3 months ago by
Cc: | RyanGlScott added |
---|
comment:6 Changed 3 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 7 weeks ago by
Cc: | vagarenko added |
---|
comment:8 Changed 5 weeks ago by
Blocked By: | 9269 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)