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

[Clinton Mead]

I've just figured that even the approach I used doesn't work very well.

Consider:

>  conditionalAdd :: Bool -> a -> Vec m a -> Vec Unknown a
>  conditionalAdd b x xs = case b of
>    True -> Runtime (x :> xs)
>    False -> Runtime xs
>
> z = init (conditionalAdd False False (True :> Nil))

'z' should be type correct, but here it's not, and there's no clear way to
do so. I guess I'd have to have a compile time type "at least of length n"
but again, I feel like this would be much cleaner with dependent types (and
perhaps a more direct translation to Haskell).

On Wed, Apr 21, 2021 at 2:55 PM Clinton Mead <clintonmead at gmail.com> wrote:

> 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/d07998bf/attachment.html>