<div dir="ltr">(replicating what i said on the ghc-devs thread)<div><br></div><div><span style="font-family:arial,sans-serif;font-size:13.333333969116211px">one thing i'm confused by, and this wasn't properly addressed in the prior threads,</span><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">
is </div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">for a type like</div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">
<br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">data Annotated t ann = MkAnn t ann</div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">
would you consider the following unsafe?</div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">instance Eq t => Eq ( Annotated t ann)</div>
<div style="font-family:arial,sans-serif;font-size:13.333333969116211px"> (==) (MkAnn t1 _) (MkAnn t2 _ ) = t1 == t2</div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">
instance Ord t => Ord (Annotated t ann)</div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px"> compare (MkAnn t1 _) (MkAnn t2 _) = compare t1 t2</div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">
<br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">by the rubric you've proposed these might be *BAD*, right? But theres many cases where you're doing computation on data, and you wish to track origin, time, etc, but these annotations are *irrelevant* for the actual values computed... It sounds like the proposal you want would rule out such instances!</div>
<div style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">your proposal would rule out these pretty natural Ord/Eq instances!</div>
<div style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">am i not understanding your proposal?</div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">
<br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">It seems like you want LVish to be deterministic in the sense of "up to equality/ordering equivalence", the computation will always yield the same answer .</div>
<div style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">Haskell has no way of enforcing totality, and deriving a "SafeEq" via generics is wrong, see the Annotated type example i made up, above.</div>
<div style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">If you define determinism up to the equivalence/ordering relations provided, and assuming anyone using LVish can read the docs before using it, is there really any real problem? are there any *real* example computations that someone might naively do despite the warning where the actual answer would be broken because of this?</div>
<div style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">If we had a richer type system (like say, Idris plus some totality info), how would we enforce the safety conditions needed to make LVish truely deterministically type safe?</div>
<div style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">cheers</div></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">
-Carter</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Oct 6, 2013 at 6:54 PM, Tillmann Rendel <span dir="ltr"><<a href="mailto:rendel@informatik.uni-marburg.de" target="_blank">rendel@informatik.uni-marburg.de</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<div class="im"><br>
<br>
Ryan Newton wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
It is very hard for me to<br>
see why people should be able to make their own Generic instances (that<br>
might lie about the structure of the type), in Safe-Haskell.<br>
</blockquote>
<br></div>
I guess that lying Generics instances might arise because of software evolution. Let's say we start with an abstract data type of binary trees.<br>
<br>
module Tree (Tree, node, empty, null, split) where<br>
data Tree a = Node (Tree a) (Tree a) | Empty<br>
deriving Generics<br>
<br>
node = Node<br>
<br>
empty = Empty<br>
<br>
null Empty = True<br>
null _ = False<br>
<br>
split (Node a b) = (a, b)<br>
<br>
size Empty = 0<br>
size (Node x y) = size x + size y<br>
<br>
Note that this data type is not really abstract, because we export the Generics instance, so clients of this module can learn about the implementation of Tree. This is not a big deal, because the chosen implementation happens to correspond to the abstract structure of binary trees anyway. So I would expect that generic code will work fine. For example, you could use generic read and show functions to serialize trees, and get a reasonable data format.<br>
<br>
Now, we want to evolve our module by caching the size of trees. We do something like this:<br>
<br>
module Tree (Tree, node, empty, null, split) where<br>
data Tree a = Tree !Int (RealTree a)<br>
<br>
data RealTree a = Node (Tree a) (Tree a) | Empty<br>
<br>
tree (Node a b) = Tree (size a + size b) t<br>
tree Empty = Tree 0 Empty<br>
<br>
node x y = tree (Node x y)<br>
<br>
empty = tree Empty<br>
<br>
null (Tree _ Empty) = True<br>
null _ = False<br>
<br>
split (Tree _ (Node a b)) = (a, b)<br>
<br>
size (Tree n _) = n<br>
<br>
Except for the Generics instance, we provide the exact same interface and behavior to our clients, we just traded some space for performance. But what Generics instance should we provide? If we just add "deriving Generics" to the two datatypes, we leak the change of representation to our clients. For example, a client that serialized a tree with a generic show function based on the old Tree cannot hope to deserialize it back with a generic read function based on the new Tree. The size information would be missing, and the structure would be different.<br>
<br>
If we write a Generics instance by hand, however, I guess we can make it present the exact same structure as the derived Generics instance for the old Tree. With this lying instance, the generic read function will happily deserialize the old data. The size will be computed on the fly, because our hand-written Generics instance will introduce calls to our smart constructors.<div class="HOEnZb">
<div class="h5"><br>
<br>
Tillmann<br>
______________________________<u></u>_________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br></div>