Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,398
    • Issues 5,398
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 590
    • Merge requests 590
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #11962
Closed
Open
Issue created Apr 20, 2016 by Richard Eisenberg@raeDeveloper

Support induction recursion

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.

Trac metadata
Trac field Value
Version 8.1
Type FeatureRequest
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
Edited Jun 17, 2019 by Ryan Scott
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking