wiki:TypeFunctions

Type Functions, Type Families, and Associated Types in GHC - The Master Plan

This page serves as a collection of notes concerning the implementation of type families (aka type functions) and associated types, especially about the implications for type checking, interface files, and FC intermediate code generation.

See the Haskell Wiki for user-level documentation.

Status

Detailed information about implemented and unimplemented features as well as bugs and plans for further improvements is at implementation status. The following provides a summary:

Implemented features:

  • All basic functionality of open data type families, open type synonym families, and equality constraints has been implemented.
  • Type checking is fully integrated with GADTs.
  • Type family instances can have ordered groups of equations. See NewAxioms.

Missing features:

  • Superclass equalities.
  • Data family instances in GADT form.
  • Re-implement functional dependencies using explicit equalities.

Speculative ideas:

  • Total type families.
  • Closed synonym families.
  • Class families.
  • Our type-indexed data types are open. However, we currently don't allow case expressions mixing constructors from different indexes. We could do that if we had a story for open function definitions outside of classes. Class instances of entire data families (including deriving clauses at family declarations to derive for all instances) requires the same sort of capabilities as case expressions mixing data constructors from different indexes. This is, as they require to build a dictionary that applies to all family instances (as opposed to a distinct dictionary per instance, which is what we have now).

Tickets

Use Keyword = TypeFamilies to ensure that a ticket ends up on these lists.

Open Tickets:

#4259
Relax restrictions on type family instance overlap
#5224
Improve consistency checking for family instances
#7102
Type family instance overlap accepted in ghci
#7808
data families and TH names do not mix well (e.g. cannot use TH deriving)
#8095
TypeFamilies painfully slow
#8109
Type family patterns should support as-patterns.
#8177
Roles for type families
#8423
Less conservative compatibility check for closed type families
#8441
Allow family instances in an hs-boot file
#9269
Type families returning quantified types
#9376
More informative error messages when closed type families fail to simplify
#9394
Show data/type family instances with ghci's :info command
#9429
Alternative to type family Any
#9562
Type families + hs-boot files = unsafeCoerce
#9667
Type inference is weaker for GADT than analogous Data Family
#9780
dep_orphs in Dependencies redundantly records type family orphans
#9898
Wanted: higher-order type-level programming
#9918
GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family
#10116
Closed type families: Warn if it doesn't handle all cases
#10141
CUSK mysteries
#10204
Odd interaction between rank-2 types and type families
#10327
Devise workaround for how infinite types prevent closed type family reduction
#10482
Not enough unboxing happens on data-family function argument
#10789
Notify user when a kind mismatch holds up a type family reduction
#10808
Odd interaction between record update and type families
#10832
Generalize injective type families
#10833
Use injective type families (decomposition) when dealing with givens
#10996
family is treated as keyword in types even without TypeFamilies enabled
#11070
Type-level arithmetic of sized-types has weaker inference power than in 7.8
#11084
Some type families don't reduce with :kind!
#11113
Type family If is too strict
#11207
GHC cannot infer injectivity on type family operating on GHC.TypeLits' Nat, but can for equivalent type family operating on user-defined Nat kind
#11243
Flag to not expand type families
#11282
Error warns about non-injectivity of injective type family
#11310
Surprising accepted constructor for GADT instance of data family
#11424
"Occurs check" not considered when reducing closed type families
#11511
Type family producing infinite type accepted as injective
#11534
Allow class associated types to reference functional dependencies
#12551
Make type indices take local constraints into account in type instance declaration
#12564
Type family in type pattern kind
#13251
Must perform family consistency check on non-imported identifiers
#13386
Poor compiler performance with type families
#13571
Injective type family syntax accepted without TypeFamilyDependencies
#13790
GHC doesn't reduce type family in kind signature unless its arm is twisted
#13809
TH-reified type familly and data family instances have a paucity of kinds
#13971
Misleading "Kind mis-match on LHS of default declaration" error
#14040
Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
#14042
Datatypes cannot use a type family in their return kind
#14111
strange error when using data families with levity polymorphism and unboxed sums and data families
#14179
"Conflicting family instance" error pretty prints data family instances poorly
#14279
Type families interfere with specialisation rewrite rules
#14319
Stuck type families can lead to lousy error messages
#14333
GHC doesn't use the fact that Coercible is symmetric
#14366
Type family equation refuses to unify wildcard type patterns
#14420
Data families should not instantiate to non-Type kinds
#14441
GHC HEAD regression involving type families in kinds

Closed Tickets:

#2721
Newtype deriving doesn't work with type families
#3990
UNPACK doesn't unbox data families
#5633
TypeFamilies don't seem to play with LIberalTypeSynonyms
#6018
Injective type families
#6035
Kind-indexed type family failure with polymorphic kinds
#6044
Regression error: Kind variables don't work inside of kind constructors in type families
#7005
GHC 7.4.2 crashes with a panic when using type families and data kinds together
#7073
Kind variable problem when declaring associated type family
#7156
"Pattern match on GADT" error for non-GADT
#7176
Failure to let kind variable remain uninstantiated when not needed
#7288
type inference fails with where clause (RankNTypes, TypeFamilies)
#7477
reifyInstances can't deal with polykinded type families
#7560
Panic in conflictInstErr when branched type family instances conflict
#7585
Core lint failure when optimizing coercions in branched axioms
#8165
Use GeneralizedNewtypeDeriving to automatically create associated type families
#8913
either bug or confusing error message mixing PolyKinds and TypeFamilies
#9582
Associated Type Synonyms do not unfold in InstanceSigs
#9747
Odd failure to deduce a constraint
#11062
Type families + hs-boot files = panic (type family consistency check too early)
#11348
Local open type families instances ignored during type checking
#11357
Regression when deriving Generic1 on poly-kinded data family
#11375
Type aliases twice as slow to compile as closed type families.
#11381
Put injective type families in a separate language extension
#11400
* is not an indexed type family
#11407
-XTypeInType uses up all memory when used in data family instance
#11708
Typechecker hangs when checking type families with -ddump-tc-trace turned on
#12057
TypeFamilyDependencies on Data.Type.Bool's `Not`
#12089
:kind command allows unsaturated type family,
#12104
Type families, `TypeError`, and `-fdefer-type-errors` cause "opt_univ fell into a hole"
#12119
Can't create injective type family equation with TypeError as the RHS
#12199
GHC is oblivious to injectivity when solving an equality constraint
#12239
Dependent type family does not reduce
#12638
GHC panic when resolving Show instance
#13025
Type family reduction irregularity (change from 7.10.3 to 8.0.1)
#13398
Associated type family instance validity checking is too conservative
#13420
Bizarre pretty-printing of closed type families in GHCi
#13774
Singletons code fails to typecheck when type signature involving type family is added
#13901
Lift the "Illegal polymorphic type" restriction on type families
#13915
GHC 8.2 regression: "Can't find interface-file declaration" for promoted data family instance
#13962
GHCi allows unsaturated type family
#13972
GHC 8.2 error message around indexes for associated type instances is baffling
#13985
GHC 8.0 regression: ‘k’ is not in scope during type checking, but it passed the renamer
#14000
Out of scope errors with type families do not mention scope
#14045
Data family instances must list all patterns of family, despite documentation's claims to the contrary
#14131
Difference between newtype and newtype instance
#14203
GHC-inferred type signature doesn't actually typecheck
#14440
Duplicate type family instances are permitted
#14462
deriving on associated data types fails to find constraints

Terminology

Data-type family: a data type declared with a data family declaration.

Type-synonym family, or type function: a type synonym declared with a type family declaration.

Type family: a data-type family or type-synonym family.

Parametric type constructors: the type constructor of a vanilla Haskell type.

Family type constructor or Family TyCon: the type constructor for a type family.

Instance TyCon: the TyCon arising from a data/newtype/type instance declaration. Sometimes called the representation TyCon. The instance TyCon is invisible to the programmer; it is only used internally inside GHC.

Associated type: A type family that is declared in a type class.

Kind signature: Declaration of the name, kind, and arity of an indexed type constructor. The arity is the number of type indexes - not the overall number of parameters - of an indexed type constructor.

Definitions vs. declarations: We sometimes call the kind signature of an indexed constructor its declaration and the subsequent population of the type family by type equations or indexed data/newtype declarations the constructor's definition.

Note: we previously used the term "indexed type", but have now switched to using "type family". Please change any uses of the former into the latter as you come across them.

How It Works

The details of the implementation are split over a couple of subpages, due to the amount of the material:

Furthermore, we have

References

  • Type Checking with Open Type Functions. Tom Schrijvers, Simon Peyton-Jones, Manuel M. T. Chakravarty, and Martin Sulzmann. In Proceedings of ICFP 2008 : The 13th ACM SIGPLAN International Conference on Functional Programming, ACM Press, pages 51-62, 2008.
  • Associated Types with Class. Manuel M. T. Chakravarty, Gabriele Keller, Simon Peyton Jones, and Simon Marlow. In Proceedings of The 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05), ACM Press, pages 1-13, 2005.
  • Associated Type Synonyms. Manuel M. T. Chakravarty, Gabriele Keller, and Simon Peyton Jones. In Proceedings of The Tenth ACM SIGPLAN International Conference on Functional Programming, ACM Press, pages 241-253, 2005.
  • Towards Open Type Functions for Haskell. Tom Schrijvers, Martin Sulzmann, Simon Peyton-Jones, and Manuel M. T. Chakravarty. Presented at IFL 2007.
  • Type Checking with Open Type Functions. Tom Schrijvers, Simon Peyton-Jones, Manuel M. T. Chakravarty, and Martin Sulzmann. ICFP 2008: The 13th ACM SIGPLAN International Conference on Functional Programming, ACM Press, 2008.
  • Old and outdated wiki material on type checking with indexed synonyms.
Last modified 9 months ago Last modified on Mar 7, 2017 10:50:47 PM