<div dir="ltr">The issue with a LiquidHaskell solution in this space, aside from the fact that it is an experiment that isn't part of the compiler or the language that we have, and uses assumptions about the way numbers work that don't hold for the ones we have, is that it is terribly invasive.<div><br></div><div>In order to use it everything that ever wants to work with your shiny new non-empty list type needs to be written in LiquidHaskell to prove the non-empty invariant still holds. Refinement types are notoriously hard to use. On the other-hand a type like NonEmpty satisfies that invariant trivially: There is no empty constructor.</div><div><br></div><div>The price of this is that it is a different data type, with different operations.</div><div><br></div><div>I love LiquidHaskell, but I'd be very hesitant to do anything or rather to not do anything predicated on its existence.</div><div><br></div><div>-Edward</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, May 4, 2015 at 2:37 PM, Reid Barton <span dir="ltr"><<a href="mailto:rwbarton@gmail.com" target="_blank">rwbarton@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><span class="">On Mon, May 4, 2015 at 12:58 PM, David Feuer <span dir="ltr"><<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>></span> wrote:<br></span><div class="gmail_extra"><div class="gmail_quote"><span class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><p dir="ltr">Wouldn't your concerns about NonEmpty be addressed by keeping its type abstract? Then something like Liquid Haskell could be used to define it better.<br></p></blockquote></span><div>There are (at least) two possible designs for a "non-empty list type".<br><br></div><div>1. A refinement type (as in LiquidHaskell) of [t] whose values include only the non-empty lists. Call it NonEmptyLiquid t. You can pass a NonEmptyLiquid t to a function that expects a [t], and you can pass a [t] to a function that expects a NonEmptyLiquid [t] if the compiler can prove that your [t] is nonempty. If it can't then you can add a runtime test for emptiness and in the non-empty case, the compiler will know the list is non-empty.<br><br></div><div>2. A new type NonEmptySolid t that is totally unrelated to [t] like you can define in Haskell today. The advantage is that NonEmptySolid is a full-fledged type constructor that can have instances, be passed to other type constructors and so on. The disadvantage is that you need to explicitly convert in your program (and possibly do a runtime conversion also) in either direction between [t] and NonEmptySolid t.<br><br></div><div>I think most people who want a "non-empty list type" want 1, not 2. Option 2 is bad for API design because it forces the users of your library to care exactly as much as you do about non-emptiness. If you imagine adding other sorts of lists like infinite lists, fixed-length or bounded-length lists, lists of even length etc. then it quickly becomes clear that having such an array of incompatible list types is not the way to go. We just want lists to be lists, but we also want the compiler to make sure we don't try to take the head of an empty list.<br><br></div><div>Those who use a NonEmpty type prefer option 2 over option 0 "type NonEmptyGas t = [t] -- and just hope"; but that doesn't mean they prefer option 2 over option 1. Those who really want option 2 can also define it as a newtype wrapper on option 1, as you noted.<br><br></div><div>So, to answer your question, no, it wouldn't really make a difference if the NonEmpty type was abstract. That would just smooth the transition to a design that I think people don't really want.<br><br></div><div>Finally, let me reiterate that there seem to be no advantages to moving a NonEmpty type into base rather than into its own small package. We don't need base to swallow up every small popular package.<br><br></div><div>Regards,<br></div><div>Reid Barton<br></div></div></div></div>
<br>_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
<br></blockquote></div><br></div>