
<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">There are good responses accruing on Reddit, so I won't repeat them here. See, in particular, /u/sccrstud92's well-explained answer at <a href="https://www.reddit.com/r/haskell/comments/mv6m5s/hacking_richard_eisenbergs_haskell_dependently/" class="">https://www.reddit.com/r/haskell/comments/mv6m5s/hacking_richard_eisenbergs_haskell_dependently/</a><div class=""><br class=""></div><div class="">There are few new points you've raised here, though:<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Apr 21, 2021, at 12:55 AM, Clinton Mead <<a href="mailto:clintonmead@gmail.com" class="">clintonmead@gmail.com</a>> wrote:</div><div class=""><div dir="ltr" class=""><div class=""><br class="">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?</div></div></div></blockquote><div><br class=""></div><div>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").</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">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?</div></div></div></blockquote><div><br class=""></div><div>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.</div><div><br class=""></div><div>I hope this helps!</div><div>Richard</div></div></div></body></html>