irrefutable patterns for existential types / GADTs

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

irrefutable patterns for existential types / GADTs

Heinrich Apfelmus
Ross Paterson wrote:
> The story so far:
> apfelmus: why are there no irrefutable patterns for GADTs?
> Conor: because you could use them to write unsafeCoerce
> Ross: how about irrefutable patterns (or newtypes) for existential types?
> Simon: Try giving the translation into System F + (existential) data types

I'd like to add that I see no problem with

   coerce :: Eq a b -> a -> b
   coerce ~Refl x = x

as long as we have

   coerce _|_ x === _|_

The wish is that

   f = \refl -> Just . coerce refl
     = \~Refl x -> Just x

should satisfy

   f _|_ x === Just _|_
   f _|_ x =/= _|_

and likewise for any other constructor than Just.

Regards,
apfelmus

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: irrefutable patterns for existential types / GADTs

Conor McBride
[hidden email] wrote:

> Ross Paterson wrote:
>  
>> The story so far:
>> apfelmus: why are there no irrefutable patterns for GADTs?
>> Conor: because you could use them to write unsafeCoerce
>> Ross: how about irrefutable patterns (or newtypes) for existential types?
>> Simon: Try giving the translation into System F + (existential) data types
>>    
>
> I'd like to add that I see no problem with
>
>    coerce :: Eq a b -> a -> b
>    coerce ~Refl x = x
>
> as long as we have
>
>    coerce _|_ x === _|_
>  

But that makes it refutable! For the above, either

  coerce _|_ x === x

or the notation is being abused.

The trouble is that GADT pattern matching has an impact on types, as
well as being a selector-destructor mechanism, and for the impact on
types to be safe, the match must be strict.

For existentials, I'm not sure, but it seems to me that there's not such
a serious issue. Isn't the only way you can use the type which allegedly
exists to project out some dictionary/other data which is packed inside
the existential? Won't this projection will cause a nice safe _|_
instead of a nasty unsafe segfault?

I think it's the extra power of GADTs to tell you more about type
variables already in play which does the damage.

All the best

Conor

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: irrefutable patterns for existential types / GADTs

Heinrich Apfelmus
> But that makes it refutable! For the above, either
>
>  coerce _|_ x === x
>
> or the notation is being abused.

Making a pattern irrefutable does not mean that the function in question
will become lazy:

  fromJust (~Just x) = x

  fromJust _|_ === _|_

The point with coerce is that it looks very much like being lazy in its
first argument but in fact it is not.

> The trouble is that GADT pattern matching has an impact on types, as
> well as being a selector-destructor mechanism, and for the impact on
> types to be safe, the match must be strict.
>
> I think it's the extra power of GADTs to tell you more about type
> variables already in play which does the damage.

But I think that something still can be squeezed out, strictness is not
absolutely necessary. I thought something along the lines of

  f :: Eq a b -> a -> Maybe b
  f ~Refl x = Just x

with

  f _|_ x  === Just _|_

The point is one can always output the constructor Just, it does not
inspect the type of x.

Now, I don't think anymore that this is feasible as the type of (Just x)
still depends on the type of x (even if the constructor Just does not
mention it). Nevertheless, I still want to remove strictness, see my
next mail in this thread.

> For existentials, I'm not sure, but it seems to me that there's not such
> a serious issue. Isn't the only way you can use the type which allegedly
> exists to project out some dictionary/other data which is packed inside
> the existential? Won't this projection will cause a nice safe _|_
> instead of a nasty unsafe segfault?

I agree. The only practical problem I can imagine is that GHC internally
treats existentials as GADTs.

Regards,
apfelmus

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: irrefutable patterns for existential types / GADTs

Heinrich Apfelmus
In reply to this post by Heinrich Apfelmus
Here is a formulation of what exactly I require from irrefutable pattern
matches for GADTs.

The problem arouse from the "Optimization problem" thread. In short,
here is a GADT-using, type safe version of Bertram's solution (without
balancing)

>      -- a binary search tree with witness about its shape
> data Map s k a where
>     Leaf :: Map () k a
>     Node :: k -> a -> Map s k a -> Map t k a -> Map (s,t) k a
>
> empty :: Map () k a
> empty = Leaf
>
> member :: Ord k => k -> Map s k a -> Bool
> member _ Leaf            = False
> member k (Node k' _ l r) = case compare k k' of
>     LT -> member k l
>     EQ -> True
>     GT -> member k r
>
>     -- a wrapper for an existential type
> data Undoer s k a where
>     Undoer :: (Map t k a) -> (Map t k a -> (a,Map s k a)) -> Undoer s k a
>
>     -- insert key element blueprint map (blueprint, result, map)
> insert :: Ord k => k -> a -> Map s k a -> Undoer s k a
> insert k a Leaf =
>    Undoer (Node k a Leaf Leaf) (\(Node k a Leaf Leaf) -> (a,Leaf))
> insert k a (Node k' b (l :: Map l k a) (r :: Map r k a) :: Map s k a)
>     = case compare k k' of
>         LT -> case insert k a l of
>                 Undoer (m :: Map t k a) f ->
>                     Undoer (Node k' b m r :: Map (t,r) k a)
>                         (\(Node k' b' m' r' :: Map (t,r) k a) ->
>                             let (a,l') = f m' in
>                               (a,Node k' b' l' r' :: Map s k a))
>         EQ -> error "inserting existing element"
>         GT -> case insert k a r of
>                 Undoer (m :: Map t k a) f ->
>                     Undoer (Node k' b l m :: Map (l,t) k a)
>                         (\(Node k' b' l' m' :: Map (l,t) k a) ->
>                             let (a,r') = f m' in
>                               (a,Node k' b' l' r' :: Map s k a))
>
>
> update :: Ord k => k -> (a -> a) -> Map s k a -> Map s k a
> -- the culprit, to be defined later
>
> splitSeq :: Ord a => [(a,b)] -> [(a,[b])]
> splitSeq = fst . splitSeq' empty
>
> splitSeq' :: Ord a => Map s a [b] -> [(a,b)] -> ([(a,[b])], Map s a [b])
> splitSeq' bp []         = ([], bp)
> splitSeq' bp ((a,b):xs) = case member a bp of
>     True -> let (l, m)  = splitSeq' bp xs in (l, update a (b:) m)
>     _    -> case insert a [] bp of
>                 Undoer bp' f -> let
>                         (rs,m)  = splitSeq' bp' xs
>                         (bs,m') = f m
>                     in ((a, b:bs) : rs, m')

To make this work in a lazy manner (it becomes an online algorithm then
and works for infinite lists), I'd like to have

> update :: Ord k => k -> (a -> a) -> Map s k a -> Map s k a
> update k f ~(Node k' a l r) = case compare k k' of
>     LT -> Node k' a (update k f l) r
>     EQ -> Node k' (f a) l r
>     GT -> Node k' a l (update k f r)

reasoning that the Node constructor should be output before one inspects
the incoming ~Node. I thought that "(l, m)  = splitSeq' bp xs" witnesses
that  bp  and  m  have the same Shape  s, but this is the point where
the not-normalizing argument throws in: the type of splitSeq' claims to
be a proof that  bp  and  m  have the same  s  but who knows whether it
really terminates?


So, I'm opting for a different update which is more along the lines of
Bertram's original:

> update :: Ord k => k -> (a -> a)
>   -> Map s k a -> Map t k a -> Map s k a
> update k f (Node k' _ l' r') ~(Node _ a l r) = case compare k k' of
>     LT -> Node k' a (update k f l' l) r
>     EQ -> Node k' (f a) l r
>     GT -> Node k' a l (update k f r)

The blueprint gives immediate witness that splitSeq' preserves shape, so
this update should be fine.



To summarize, the main problem is to get a lazy/online algorithm (the
problem here falls into the "more haste, less speed" category) while
staying more type safe.
@Conor: how does this issue look like in Epigram?

Regards,
apfelmus

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: irrefutable patterns for existential types / GADTs

Conor McBride
Hi

[hidden email] wrote:
> To summarize, the main problem is to get a lazy/online algorithm (the
> problem here falls into the "more haste, less speed" category) while
> staying more type safe.
> @Conor: how does this issue look like in Epigram?
>  

Thanks for asking!

In the current Epigram prototype editor/checker, nothing clever happens.
Apart from anything else, typechecking relies on /partial/ evaluation,
so we can't presume that the only normal forms in a datatype are made
with constructors: they might be expressions which have got stuck.

However, Edwin Brady's prototype compiler delivers code for
run-time-only usage, and here we begin to get paid for working in a
total (once suitably stratified) language. It isn't necessary to perform
constructor discrimination when it's statically known that exactly one
constructor is possible, so those patterns can always be made
irrefutable, with matching replaced by projection. It's not yet obvious
whether this is always, never, predictably sometimes, or unpredictably
sometimes a good idea. However, we'd certainly be able to support an
explicit notation for irrefutable patterns, guaranteed to match whenever
the named subobjects were needed.

So we don't just give that coerce example an irrefutable pattern, we can
erase all run-time trace of equality evidence, and indeed any other data
whose value is completely determined by the indices of its type. If you
don't need to discriminate on it, you don't need to look at it, so you
don't need to keep it.

Even though type-vs-value distinction no longer aligns with the
static-vs-dynamic distinction, you don't get any less run-time
type-erasure. You should actually get more run-time value-erasure!

Online algorithms do look like a good place to try to get some leverage
from this, but we haven't really been in a position to experiment so
far. I'm sure that will change.

All the best

Conor



This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: irrefutable patterns for existential types / GADTs

Heinrich Apfelmus
> Thanks for asking!
> [...]
> Online algorithms do look like a good place to try to get some leverage
> from this, but we haven't really been in a position to experiment so
> far. I'm sure that will change.

Well, I asked because laziness with memoization gives a definite edge in
terms of algorithmic time complexity over strictness (proved for online
algorithms in "more haste, less speed") and I wonder how this goes
together with totality and dependent types. A forthcoming ultimate
programming language should retain this edge, shouldn't it? ;-)


> It isn't necessary to perform
> constructor discrimination when it's statically known that exactly one
> constructor is possible, so those patterns can always be made
> irrefutable, with matching replaced by projection.

Thanks for pinpointing the culprit, because translated to GADTs, it
means that

    "whenever we know from the type index that only one constructor is
possible, it can be made irrefutable."

So this is the kind of irrefutable pattern one could safely add. In
particular, this can be weakened to

    "whenever we know the type index, i.e. there is no type refinement
depending on the value, an irrefutable pattern is safe."

But once no type refinement happens, the irrefutable pattern can already
be obtained via let bindings in existing Haskell! Below is a lazy
version of Bertram solution to the "Optimization problem" following
Ross' suggestions with existentials and GADTs:

> {-# OPTIONS_GHC -fglasgow-exts #-}
>
> data Map s k a where
>     Leaf :: Map () k a
>     Node :: k -> a -> Map s k a -> Map t k a -> Map (s,t) k a

(Map s k a) is a tree which makes its structure explicit in the type
index s.

>
> unNode :: Map (s,t) k a -> (k,a,Map s k a, Map t k a)
> unNode (Node k a l r) = (k,a,l,r)

unNode knows the type index and is to be used for a lazy pattern match
  let (k,a,l,r) = unNode ..

> empty :: Map () k a
> empty = Leaf
>
> member :: Ord k => k -> Map s k a -> Bool
> member _ Leaf            = False
> member k (Node k' _ l r) = case compare k k' of
>     LT -> member k l
>     EQ -> True
>     GT -> member k r
>
> data Undoer s k a where
>     Undoer :: (Map t k a) -> (Map t k a -> (a,Map s k a)) -> Undoer s k a

Undoer is just (exists t. ...) wrapped into a digestible type.

>     -- insert key element blueprint map (blueprint, result, map)
> insert :: Ord k => k -> a -> Map s k a -> Undoer s k a
> insert k a Leaf = Undoer (Node k a Leaf Leaf)
>     (\map -> let (_,a,_,_) = unNode map in (a,Leaf))

Note how the type system proves that the function (\map -> ..) always
has to expect (map) == Node ...
Then, unNode binds k',b',... /lazily/.
Same goes for the rest of insert:

> insert k a (Node k' b (l :: Map l k a) (r :: Map r k a) :: Map s k a)
>     = case compare k k' of
>         LT -> case insert k a l of
>             Undoer (m :: Map t k a) f ->
>                 Undoer (Node k' b m r :: Map (t,r) k a)
>                     (\map -> let
>                             (k',b',m',r') = unNode map
>                             (a,l') = f m'
>                         in (a,Node k' b' l' r' :: Map s k a))
>         EQ -> error "inserting existing element"
>         GT -> case insert k a r of
>             Undoer (m :: Map t k a) f ->
>                 Undoer (Node k' b l m :: Map (l,t) k a)
>                     (\map -> let
>                             (k',b',l',m') = unNode map
>                             (a,r') = f m'
>                         in (a,Node k' b' l' r' :: Map s k a))
>
>     -- update k fun blueprint map
> update :: Ord k => k -> (a -> a) -> Map s k a -> Map s k a -> Map s k a
> update k f (Node k' _ l' r') map = case compare k k' of
>     LT -> Node k' a (update k f l' l) r
>     EQ -> Node k' (f a) l r
>     GT -> Node k' a l (update k f r' r)
>     where
>     (_,a,l,r) = unNode map

Again a lazy pattern match on (map). Note that the type system enforces
that blueprint and actual (map) have the same shape s. The type
refinement for GADTs happens in the strict pattern match on the
blueprint and this allows us to lazily match the (map).

> splitSeq :: Ord a => [(a,b)] -> [(a,[b])]
> splitSeq = fst . splitSeq' empty
>
> splitSeq' :: Ord a => Map s a [b] -> [(a,b)] -> ([(a,[b])], Map s a [b])
> splitSeq' bp []         = ([], bp)
> splitSeq' bp ((a,b):xs) = case member a bp of
>     True -> let (l, m)  = splitSeq' bp xs in (l, update a (b:) bp m)
>     _    -> case insert a [] bp of
>                 Undoer bp' f -> let
>                         (rs,m)  = splitSeq' bp' xs
>                         (bs,m') = f m
>                     in ((a, b:bs) : rs, m')

To summarize, the problem can be solved without irrefutable patterns for
GADTs: the code above works for infinite lists. Yet, they are handy and
can be introduced safely in the case where the type indices are known in
advance and no type refinement happens.

Regards,
apfelmus

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe