<p>I know about some of the potential advantages and the desirable features of Agda/Coq/F*/Idris2, etc. But what about the other side of things? For example, there seems to have been talk for years about 'dependent Haskell' but AFAIK it hasn't come to fruition as yet.</p>

<types><haskell><dependent-types>
What are some of the challenges in implementing, and disadvantages of having, dependent types in a programming language?
CC BY-SA 4.0
2024-05-26T13:49:24.460Z
There are many different ways for a programming language to ben dependently types. Two axes are (1) how expressive should the type dependency be (this typically dictates how much type inference can be done automatically)? (2) What is the intention of the type dependency (e.g. do you want the language to be a Curry-Howard-Lambek style theorem prover, or do you not care about consistency)? That affects if you can have   full recursion of exceptions.
Martin Berger
CC BY-SA 4.0
2024-05-26T15:40:36.253Z
Dependent Haskell is a complicated case, because the dependent types need to be compatible with a large number of existing extensions to the Haskell type system, which include things like linear types and impredicative polymorphism. It also needs to be compatible with the way in which types often erased (and invisible) in Haskell as currently used. For the last point, see [this proposal](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst) which describes six different kinds of universal quantification, 3 of which are already in Haskell.
David Young
CC BY-SA 4.0
2024-05-28T00:26:08.267Z
There is a huge difference between designing a dependently-typed programming language (e.g. Agda, Coq, F*, Idris, GURU, …) and bolting dependent types onto an existing programming language with an extremely complex and rich existing type system that was never meant to have dependent types, plus extending the core and standard libraries with dependent types without breaking any existing language extension, type system feature, and library or third-party user code.
Jörg W Mittag
CC BY-SA 4.0
2024-05-28T06:50:19.900Z
@JörgWMittag good point. Sorry I didn't mean to imply that Haskell was somehow 'at fault' for not having dependent types; I suppose in the Haskell case I wonder(ed) whether there is in fact consensus (within Haskell community) that dependent types would be a good thing if implementing them in the language was not so logistically difficult.
Municipal-Chinook-7
CC BY-SA 4.0
2024-05-28T12:55:27.257Z
And I didn't mean to imply that you meant to imply that :-D I just wanted to point out that designing a dependently-typed language from scratch, adding dependent types to a language not originally meant to have them, and *implementing* dependent types are three separate concerns. Maybe it would make sense to clarify which of the three you are most interested in and/or split the question accordingly.
Jörg W Mittag
# What are some of the challenges in implementing, and disadvantages of having, dependent types in a programming language?
Posted by: username_0 on 2024-05-26
I know about some of the potential advantages and the desirable features of Agda/Coq/F\*/Idris2, etc. But what about the other side of things? For example, there seems to have been talk for years about 'dependent Haskell' but AFAIK it hasn't come to fruition as yet.
**Tags:** types haskell dependent-types
> **Comments:**
> **username_1**: There are many different ways for a programming language to ben dependently types. Two axes are (1) how expressive should the type dependency be (this typically dictates how much type inference can be done automatically)? (2) What is the intention of the type dependency (e.g. do you want the language to be a Curry-Howard-Lambek style theorem prover, or do you not care about consistency)? That affects if you can have   full recursion of exceptions.  
> **username_2**: Dependent Haskell is a complicated case, because the dependent types need to be compatible with a large number of existing extensions to the Haskell type system, which include things like linear types and impredicative polymorphism. It also needs to be compatible with the way in which types often erased (and invisible) in Haskell as currently used. For the last point, see [this proposal](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst) which describes six different kinds of universal quantification, 3 of which are already in Haskell.  
> **username_3**: There is a huge difference between designing a dependently-typed programming language (e.g. Agda, Coq, F*, Idris, GURU, …) and bolting dependent types onto an existing programming language with an extremely complex and rich existing type system that was never meant to have dependent types, plus extending the core and standard libraries with dependent types without breaking any existing language extension, type system feature, and library or third-party user code.  
> **username_0**: @JörgWMittag good point. Sorry I didn't mean to imply that Haskell was somehow 'at fault' for not having dependent types; I suppose in the Haskell case I wonder(ed) whether there is in fact consensus (within Haskell community) that dependent types would be a good thing if implementing them in the language was not so logistically difficult.  
> **username_3**: And I didn't mean to imply that you meant to imply that :-D I just wanted to point out that designing a dependently-typed language from scratch, adding dependent types to a language not originally meant to have them, and *implementing* dependent types are three separate concerns. Maybe it would make sense to clarify which of the three you are most interested in and/or split the question accordingly.  
---
## 0 answers
