[GHC] #11962: Support induction recursion

20 Apr 2016

      #11962: Support induction recursion
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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
 [wiki:DependentHaskell/Internal#Separatingtypesignaturesfromdefinitions
 here].

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11962
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler