In Haskell, GADTs are only indexed by types, while indexed families in DT are mainly indexed by terms. With the presence of without-K, it is hard to refute cases just by unifying type terms, while in Haskell the situation is essentially different, where the only way to refute cases is by unifying type terms.

Am I thinking about them correctly? Is there any literature about this?

  • $\begingroup$ This is impentrable to me as a non haskeller what do you mean by "without-K"? $\endgroup$ Commented Jun 23, 2023 at 22:46
  • $\begingroup$ @BruceAdams K is the eliminator for the type x = x, for a fixed variable x, compared to J, an eliminator of Σy. x = y, for a fixed x. K is incompatible with univalence, so if you want univalence you'll need to disable K. There is a non-trivial consequence of this: you can't simply unify types, because there can be non-trivial paths between them (while if you're sure a type is an h-set, then you can still unify them). The standard reference to this is Jesper Cockx's paper "Eliminating dependent pattern matching without K" $\endgroup$
    – ice1000
    Commented Jun 23, 2023 at 23:34
  • 1
    $\begingroup$ Thank you for clearing that up - i.etsystatic.com/12253060/r/il/1ce2d4/2767067032/… $\endgroup$ Commented Jun 23, 2023 at 23:44
  • $\begingroup$ Your comment also reminds me of this - stackoverflow.com/q/3870088/1569204 :) (I am trying to learn more type theory but I have a busy life and its slow going) $\endgroup$ Commented Jun 23, 2023 at 23:47
  • 1
    $\begingroup$ Tangentially related question I asked on CS SE a few years ago: cs.stackexchange.com/questions/132664/… $\endgroup$
    – Alexis King
    Commented Jun 28, 2023 at 4:56


You must log in to answer this question.

Browse other questions tagged .