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

[Clinton Mead]

My apologies for the (kind of) cross post, I originally put a similar
question on the Haskell
<https://www.reddit.com/r/haskell/comments/mv6m5s/hacking_richard_eisenbergs_haskell_dependently/>
Reddit
<https://www.reddit.com/r/haskell/comments/mv6m5s/hacking_richard_eisenbergs_haskell_dependently/>
I'm never sure the best place to post these sorts of things.

Inspired by some of the code
<https://github.com/goldfirere/video-resources/tree/main/2021-04-20-vectors>
from one of Richard Eisenberg's weekly videos
<https://www.youtube.com/watch?v=WHeBxSBY0fc> (which I always eagerly
await!) I made some adjustments to his code here
<https://gist.github.com/clintonmead/dc6233afb14cb04a3e1ae2b44bd0bf08>.

Basically the attempt is to be able to deal with compile time known length
lists and runtime only known length lists as uniformly as possible, as the
logic is the same in both cases. In addition, allowing us to do things like
`safeHead (x : xs)` regardless whether we know the length of `xs` at
runtime or compile time, because it should never fail.

My attempt makes things a bit messier, adding an extra constructor in the
runtime case, and then naturally this means all the functions have to be
extended to specifically pattern matched on this constructor.

I'm trying to wrap my head around dependent types, and I did buy the ebook
version of "Type-Driven Development in Idris", but I've never used Idris
before so perhaps I'm having some trouble making these examples more
concrete.

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?

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?

Thanks,
Clinton
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210421/c54d3b16/attachment.html>