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 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_... Reddit https://www.reddit.com/r/haskell/comments/mv6m5s/hacking_richard_eisenbergs_... 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