[Haskell-cafe] Richard Eisenberg inspired dependent type hacking and some questions
clintonmead at gmail.com
Wed Apr 21 06:51:48 UTC 2021
I've just figured that even the approach I used doesn't work very well.
> 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
> I'm never sure the best place to post these sorts of things.
> Inspired by some of the code
> 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
> 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
> 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?
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe