<p>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.</p>
<p>Am I thinking about them correctly? Is there any literature about this?</p>

<algebraic-data-types><gadt>
How does GADTs as in Haskell-like languages compare to indexed families in dependent types?
CC BY-SA 4.0
2023-06-23T22:46:18.377Z
This is impentrable to me as a non haskeller what do you mean by "without-K"?
Bruce Adams
CC BY-SA 4.0
2023-06-23T23:34:26.513Z
@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"
ice1000
CC BY-SA 4.0
2023-06-23T23:44:15.877Z
Thank you for clearing that up - https://i.etsystatic.com/12253060/r/il/1ce2d4/2767067032/il_1140xN.2767067032_9vel.jpg
Bruce Adams
CC BY-SA 4.0
2023-06-23T23:47:30.030Z
Your comment also reminds me of this - https://stackoverflow.com/q/3870088/1569204 :)  (I am trying to learn more type theory but I have a busy life and its slow going)
Bruce Adams
CC BY-SA 4.0
2023-06-24T00:03:54.400Z
That's just a meme, I'm trying to be serious.
ice1000
CC BY-SA 4.0
2023-06-24T00:11:43.387Z
No offence intended. There are many great questions that can benefit from more background. Adding more background helps if you are within the target audience but sometimes it just highlights more gaps in one's knowledge.
Bruce Adams
CC BY-SA 4.0
2023-06-28T04:56:11.100Z
Tangentially related question I asked on CS SE a few years ago: https://cs.stackexchange.com/questions/132664/relationship-between-inductive-families-and-type-returning-functions
Alexis King
# How does GADTs as in Haskell-like languages compare to indexed families in dependent types?
Posted by: username_0 on 2023-06-23
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?
**Tags:** algebraic-data-types gadt
> **Comments:**
> **username_1**: This is impentrable to me as a non haskeller what do you mean by "without-K"?  
> **username_0**: @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"  
> **username_1**: Thank you for clearing that up - https://i.etsystatic.com/12253060/r/il/1ce2d4/2767067032/il_1140xN.2767067032_9vel.jpg  
> **username_1**: Your comment also reminds me of this - https://stackoverflow.com/q/3870088/1569204 :)  (I am trying to learn more type theory but I have a busy life and its slow going)  
> **username_0**: That's just a meme, I'm trying to be serious.  
> **username_1**: No offence intended. There are many great questions that can benefit from more background. Adding more background helps if you are within the target audience but sometimes it just highlights more gaps in one's knowledge.  
> **username_2**: Tangentially related question I asked on CS SE a few years ago: https://cs.stackexchange.com/questions/132664/relationship-between-inductive-families-and-type-returning-functions  
---
## 0 answers
