Skip to content

Instantly share code, notes, and snippets.

@Icelandjack
Created November 12, 2016 23:33
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save Icelandjack/660ccce86d4461fd467638368f0d1ac2 to your computer and use it in GitHub Desktop.
Type Families

Total Type Families

A total type family feels quite comfortable. By total here, I mean a type family whose equations cover all the possible cases and which is guaranteed to terminate. That is, a total type family is properly a function on types. Those other dependently typed languages have functions on types, and they seem to work nicely. I am completely unbothered by total type families.

What are type families?

Non-covering Type Families (are strange)

A non-covering type family is a type family whose patterns do not cover the whole space. Let’s consider closed and open families separately, because the issues that come up are different.

What are type families?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment