Skip to content

GitLab

  • Menu
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 4,867
    • Issues 4,867
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 457
    • Merge requests 457
  • 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 Compiler
  • GHCGHC
  • Issues
  • #19238
Closed
Open
Created Jan 19, 2021 by Sylvain Henry@hsyl20Developer

Recursive type families optimisation

Motivation

Consider the following simple example:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Foo where

import GHC.TypeNats

type family Index n xs where
    Index 0 (x:_)  = x
    Index n (_:xs) = Index (n-1) xs


x :: Index 2 '[Float,Int,Bool]
x = True

It results in a lot of bloat in Core:

-- RHS size: {terms: 1, types: 0, coercions: 56, joins: 0/0}
x :: Index 2 '[Float, Int, Bool]
[GblId,
 Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)
         Tmpl= GHC.Types.True
               `cast` (Sub (Sym (Foo.D:R:Index[0] <Bool>_N <'[]>_N))
                       ; (Index (Sym (SubDef (<1>_N, <1>_N))) <'[Bool]>_N)_R
                       ; Sub (Sym (Foo.D:R:Index[1] <1>_N <Int>_N <'[Bool]>_N))
                       ; (Index (Sym (SubDef (<2>_N, <1>_N))) <'[Int, Bool]>_N)_R
                       ; Sub (Sym (Foo.D:R:Index[1] <2>_N <Float>_N <'[Int, Bool]>_N))
                       :: Bool ~R# Index 2 '[Float, Int, Bool])}]
x = GHC.Types.True
    `cast` (Sub (Sym (Foo.D:R:Index[0] <Bool>_N <'[]>_N))
            ; (Index (Sym (SubDef (<1>_N, <1>_N))) <'[Bool]>_N)_R
            ; Sub (Sym (Foo.D:R:Index[1] <1>_N <Int>_N <'[Bool]>_N))
            ; (Index (Sym (SubDef (<2>_N, <1>_N))) <'[Int, Bool]>_N)_R
            ; Sub (Sym (Foo.D:R:Index[1] <2>_N <Float>_N <'[Int, Bool]>_N))
            :: Bool ~R# Index 2 '[Float, Int, Bool])

The number of coercions balloons quickly:

Type # coercions
Index 1 '[Float,Bool] 28
Index 2 '[Float,Char,Bool] 56
Index 3 '[Float,Char,Int,Bool] 90
Index 4 '[Float,Char,Int,String,Bool] 134

Now if we also define y = x we get:

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
y :: Bool
[GblId,
 Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)
         Tmpl= GHC.Types.True}]
y = GHC.Types.True

GHC has dropped the coercion!

Proposal

  1. Ideally x should be automatically rewritten exactly as y (i.e., coercions should be dropped when possible).
  2. We could perhaps avoid role conversions on every Coercion (e.g. by doing the whole chain of TransCo nominally and then only Subing at the end)
  3. Perhaps add Sym as a boolean field of common coercions and axioms (FunCo, SubDef, etc.) to avoid an indirection
  4. Coercions are currently LCF-like proofs. It could be worth trying to store them as tactics instead: for example replacing the chain of instantiated type family application coercions (e.g. Index (Sym (SubDef (<2>_N, <1>_N))) <'[Int, Bool]>_N) with a more generic Reduce with Index n times on the RHS.
Edited Jan 19, 2021 by Sylvain Henry
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking