[Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

[Carter Schonwald]

(replicating what i said on the ghc-devs thread)

one thing i'm confused by, and this wasn't properly addressed in the prior
threads,
is

for a type like

data Annotated t ann =  MkAnn t ann

would you consider the following unsafe?

instance Eq t => Eq ( Annotated t ann)
   (==) (MkAnn t1 _) (MkAnn t2 _ ) =  t1 == t2

instance Ord t => Ord (Annotated t ann)
  compare (MkAnn t1 _) (MkAnn t2 _) = compare t1 t2

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!

your proposal would rule out these pretty natural Ord/Eq instances!

am i not understanding your proposal?

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 .

Haskell has no way of enforcing totality, and deriving a "SafeEq" via
generics is wrong, see the Annotated type example i made up, above.

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?

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?

cheers
-Carter


On Sun, Oct 6, 2013 at 6:54 PM, Tillmann Rendel <
rendel at informatik.uni-marburg.de> wrote:

> Hi,
>
>
> Ryan Newton wrote:
>
>> It is very hard for me to
>> see why people should be able to make their own Generic instances (that
>> might lie about the structure of the type), in Safe-Haskell.
>>
>
> 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.
>
>   module Tree (Tree, node, empty, null, split) where
>     data Tree a = Node (Tree a) (Tree a) | Empty
>       deriving Generics
>
>     node = Node
>
>     empty = Empty
>
>     null Empty = True
>     null _ = False
>
>     split (Node a b) = (a, b)
>
>     size Empty = 0
>     size (Node x y) = size x + size y
>
> 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.
>
> Now, we want to evolve our module by caching the size of trees. We do
> something like this:
>
>   module Tree (Tree, node, empty, null, split) where
>     data Tree a = Tree !Int (RealTree a)
>
>     data RealTree a = Node (Tree a) (Tree a) | Empty
>
>     tree (Node a b) = Tree (size a + size b) t
>     tree Empty = Tree 0 Empty
>
>     node x y = tree (Node x y)
>
>     empty = tree Empty
>
>     null (Tree _ Empty) = True
>     null _ = False
>
>     split (Tree _ (Node a b)) = (a, b)
>
>     size (Tree n _) = n
>
> 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.
>
> 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.
>
>
>   Tillmann
> ______________________________**_________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20131006/86c08c5d/attachment.htm>