<div dir="ltr">I've just figured that even the approach I used doesn't work very well.<div><br></div><div>Consider:</div><div><br></div><div>

> 

conditionalAdd :: Bool -> a -> Vec m a -> Vec Unknown a<br>

> 

conditionalAdd b x xs = case b of<br>

> 

  True -> Runtime (x :> xs)<br>

> 

  False -> Runtime xs<br>> <br>> z = init (conditionalAdd False False (True :> Nil))<br></div><div><br></div><div>'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). </div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Apr 21, 2021 at 2:55 PM Clinton Mead <<a href="mailto:clintonmead@gmail.com">clintonmead@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>My apologies for the (kind of) cross post, I originally put a similar question on the <a href="https://www.reddit.com/r/haskell/comments/mv6m5s/hacking_richard_eisenbergs_haskell_dependently/" target="_blank">Haskell </a><a href="https://www.reddit.com/r/haskell/comments/mv6m5s/hacking_richard_eisenbergs_haskell_dependently/" target="_blank">Reddit</a> I'm never sure the best place to post these sorts of things.</div><div><br></div><div>Inspired by some of the <a href="https://github.com/goldfirere/video-resources/tree/main/2021-04-20-vectors" target="_blank">code</a> from one of Richard Eisenberg's weekly <a href="https://www.youtube.com/watch?v=WHeBxSBY0fc" target="_blank">videos</a> (which I always eagerly await!) I made some adjustments to his code <a href="https://gist.github.com/clintonmead/dc6233afb14cb04a3e1ae2b44bd0bf08" target="_blank">here</a>.</div><div><br></div><div>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. </div><div><br></div><div>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.</div><div><br></div><div>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. </div><div><br>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><br></div><div>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><br></div><div>Thanks,</div><div>Clinton</div></div>
</blockquote></div>