[Haskell-cafe] Richard Eisenberg inspired dependent type hacking and some questions

[Richard Eisenberg]

There are good responses accruing on Reddit, so I won't repeat them here. See, in particular, /u/sccrstud92's well-explained answer at https://www.reddit.com/r/haskell/comments/mv6m5s/hacking_richard_eisenbergs_haskell_dependently/ <https://www.reddit.com/r/haskell/comments/mv6m5s/hacking_richard_eisenbergs_haskell_dependently/>

There are few new points you've raised here, though:

> On Apr 21, 2021, at 12:55 AM, Clinton Mead <clintonmead at gmail.com> wrote:
> 
> The vague idea I've seemed to have heard is that dependent types blurs the distinction between "values" and "types", so in Idris my thought was as a result we get rid of this messy hacky distinction between the two that's required in Haskell. Can we actually do this and how?

Having dependent types means that we don't need singletons, because e.g. the `n` in `SNat n` would be available both at runtime and at compile time. Really, when we say that dependent types blur values and types, we really mean that it allows the same data to be available at runtime (sometimes called "values") and compile-time (sometimes called "types").

> 
> And indeed, can we do this in Haskell as well? Does the current GHC type system give us tools to allow what I've designed without bloating all the functions by having to deal with this extra constructor match?

Existentials are the way to do this. Haskell's support for existentials is similar to that in Idris -- the issue there isn't really about dependent types, per se.

I hope this helps!
Richard
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210421/9f4dd303/attachment.html>