Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,265
    • Issues 4,265
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 421
    • Merge Requests 421
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #11962

Closed
Open
Opened 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
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#11962