We hope to have a friendly document explaining everything new Darcs developers or Darcs library users need to know about type witnesses.

Background

TODO: what problem are we trying to solve by using witnesses?

Overview

• What values do the wX etc type variables get instantiated to?

Big Ideas

• Phantom types
• Existential types
• Type families

Core concepts

FL vs RL

Sealing

Gaps

IsEq

unsafeCoerce

What do I do with?

Fragments of explanations

Here are little fragments from our past that point in that direction. We need a proper comprehensive document in the long run.

• Sealing patches:

  • Seal and FlippedSeal
  • “when you seal a patch, you agree to lose information about it”
• Phantom Types, Existentials and Controlling Unification

• the point of IsEq

• see thread parent for the context, and an example of why you’d want something like IsEq

• Talk about use of GADTs to provide witnesses

See also

• Historical plan
• Jason Dagit’s Master’s Thesis
  • probably the most comprehensive document you’ll find for now