how to nicely implement phantom type coersion?

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

how to nicely implement phantom type coersion?

David Roundy
Hello all,

I've been working on a sort of static consistency-checking framework for
darcs patches using GADTs and phantom existential types, and am looking for
a bit of advice on whether I might be able to create a class to avoid some
tedious coding overhead.

The basic idea is that a patch will have type (Patch a b) where "a" and "b"
are phantom types.  Sequential patches will have identical ending and
beginning types.  So that a sequential pair, for example, can be written as

data Sequential a c where
    Sequential :: Patch a b -> Patch b c -> Sequential a c

The trickiness is that we need to be able to check for equality of two
patches, and if they are truly equal, then we know that their ending states
are also equal.  We do this with a couple of operators:

    (=\/=) :: Patch a b -> Patch a c -> Maybe (EqContext b c)
    (=/\=) :: Patch a z -> Patch b z -> Maybe (EqContext a b)

data EqContext a b =
    EqContext { coerce_start :: Patch a z -> Patch b z,
                coerce_end :: Patch z a -> Patch z b,
                backwards_coerce_start :: Patch b z -> Patch a z,
                backwards_coerce_end :: Patch z b -> Patch z a
              }

where we use the EqContext to encapsulate unsafeCoerce so that it can only
be used safely.  The problem is that it's tedious figuring out whether to
use coerce_start or coerce_end, or backwards_coerce_end, etc.  Of course,
the huge advantage is that you can't use these functions to write buggy
code (at least in the sense of breaking the static enforcement of patch
ordering).

So I'm wondering if there might be some sort of multi-parameter class one
could define that would ease the use of an EqContext.  For example I can
imagine a (somewhat lame) class

class EqTypes a b where
   safe_coerce_end :: Patch x a -> Patch x b
   safe_coerce_start :: Patch x a -> Patch x b
   safe_coerce_start = invert $ safe_coerce_end $ invert p

(note that invert :: Patch a b -> Patch b a)

then we could perhaps write some template haskell to define a couple of
instances of EqTypes from a data type EqContext... except that I suspect
that this is isn't possible, since the EqContext only exists at runtime, so
unless one could define classes dynamically at runtime I'm out of luck.

So is there some other approach that I can use for easily coercing phantom
types based on runtime checks? Any suggestions?

What I'd really love would be to be able to create a function that is
polymorphic in kind rather than in type such as (inventing a rather poor
syntax off the top of my head):

data EqContext a b = EqContext { safe_coerce :: f(a,b) -> f(b,a) }

where f(a,b) is a function of two types that returns a type, so the value
of f(a,b) might be (Patch a b) or (Patch x b) or something like that.

But I'm not sure if this is possible in Haskell, and if it is, then it
definitely requires some sort of tricky extension that I'm not familiar
with...
--
David Roundy
http://www.darcs.net
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: [darcs-conflicts] how to nicely implement phantom type coersion?

Ian Lynagh
On Thu, Dec 08, 2005 at 09:23:22AM -0500, David Roundy wrote:
>
> data EqContext a b = EqContext { safe_coerce :: f(a,b) -> f(b,a) }
>
> where f(a,b) is a function of two types that returns a type, so the value
> of f(a,b) might be (Patch a b) or (Patch x b) or something like that.
>
> But I'm not sure if this is possible in Haskell, and if it is, then it
> definitely requires some sort of tricky extension that I'm not familiar
> with...

I'm a bit confused, but if you have:

sc :: p a b -> p a c
sc = unsafeCoerce#

then (with Either standing in for Patch, PatchList etc and some concrete
types as parameters to simplify things)

sc (undefined :: Either Int Char) :: Either Int Bool

is well-typed but

sc (undefined :: Either Int Char) :: Either String Char

isn't. Is that what you want?


Thanks
Ian

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

Re: Re: [darcs-conflicts] how to nicely implement phantom type coersion?

Ralf Hinze
> > data EqContext a b = EqContext { safe_coerce :: f(a,b) -> f(b,a) }

I haven't seen the original post, so take the following with a
grain of salt. It seems that you are looking for a type that
models safe coercions. Here is one, the type a :=: b defined below
goes back to  Leibniz's principle of substituting equals for equals:
in every context `f' you can replace an `a' by a `b'.

Cheers, Ralf

---

Type equality.

> module TypeEq ((:=:), refl, symm, trans, (<>), list, pair, coerce, from, to)
> where

The type of type equality: |a :=: b| is non-empty iff |a = b|.

> newtype a :=: b               =  Proof { apply :: forall f . f a -> f b }

Equality is reflexive, symmetric, transitive and congruent.

> refl                          :: forall a . a :=: a
> refl                          =  Proof id
>
> newtype Flip f a b            =  Flip { unFlip :: f b a }
>
> symm                          :: forall a b . a :=: b -> b :=: a
> symm p                        =  unFlip (apply p (Flip refl))
>
> trans                         :: forall a b c . a :=: b -> b :=: c -> a :=: c
> trans p q                     =  Proof (apply q . apply p)
>
> (<>)                          =  trans
>
> newtype List f a              =  List { unList :: f [a] }
>
> list                          :: a :=: b -> [a] :=: [b]
> list p                        =  Proof (unList . apply p . List)
>
> newtype Pair1 f b a           =  Pair1 { unPair1 :: f (a, b)}
> newtype Pair2 f a b           =  Pair2 { unPair2 :: f (a, b)}
>
> pair                          :: a :=: c -> b :=: d -> (a, b) :=: (c, d)
> pair p1 p2                    =  Proof (unPair2 . apply p2 . Pair2 . unPair1 . apply p1 . Pair1)

Special casts.

> coerce                        =  apply
>
> newtype Id a                  =  Id { unId :: a }
>
> from                          :: forall a b . a :=: b -> (a -> b)
> from ep                       =  \ a -> unId (apply ep (Id a))
>
> newtype Inv a b               =  Inv { unInv :: b -> a }
>
> to                            :: forall a b . a :=: b -> (b -> a)
> to ep                         =  unInv (apply ep (Inv id))
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: [darcs-conflicts] how to nicely implement phantom type coersion?

Taral
In reply to this post by David Roundy
On 12/8/05, David Roundy <[hidden email]> wrote:
> So is there some other approach that I can use for easily coercing phantom
> types based on runtime checks? Any suggestions?

None here. Since H-M uses type unification to do type inference, you
can't auto-create a program based on the inferred types around it.

--
Taral <[hidden email]>
"Computer science is no more about computers than astronomy is about
telescopes."
    -- Edsger Dijkstra
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: how to nicely implement phantom type coersion?

Thomas Jaeger-3
In reply to this post by David Roundy
Hello,

Since you're already using GADTs, why not also use them to witness type
equality:

import GHC.Exts

data Patch a b = Patch Int Int

data Sequential a c where
    Sequential :: Patch a b -> Patch b c -> Sequential a c

data MaybeEq :: * -> * -> * where
  NotEq :: MaybeEq a b
  IsEq  :: MaybeEq a a

(=//=) :: Patch a b -> Patch c d -> MaybeEq b c
Patch _ x =//= Patch y _
  | x == y    = unsafeCoerce# IsEq
  | otherwise = NotEq

sequenceIfPossible :: Patch a b -> Patch c d -> Maybe (Sequential a d)
sequenceIfPossible p q
  | IsEq <- p =//= q = Just $ Sequential p q
  | otherwise        = Nothing

Notice the usefulness of pattern guards. EqContext could be defined as

data EqContext :: * -> * -> * where
  EqWitness :: EqContext a a

(though I ususally prefer to just call both the data type and the
constructor 'E'.)


Thomas

On Thu, 2005-12-08 at 09:23 -0500, David Roundy wrote:

> The trickiness is that we need to be able to check for equality of two
> patches, and if they are truly equal, then we know that their ending states
> are also equal.  We do this with a couple of operators:
>
>     (=\/=) :: Patch a b -> Patch a c -> Maybe (EqContext b c)
>     (=/\=) :: Patch a z -> Patch b z -> Maybe (EqContext a b)
>
> data EqContext a b =
>     EqContext { coerce_start :: Patch a z -> Patch b z,
>                 coerce_end :: Patch z a -> Patch z b,
>                 backwards_coerce_start :: Patch b z -> Patch a z,
>                 backwards_coerce_end :: Patch z b -> Patch z a
>               }
>
> where we use the EqContext to encapsulate unsafeCoerce so that it can only
> be used safely.  The problem is that it's tedious figuring out whether to
> use coerce_start or coerce_end, or backwards_coerce_end, etc.  Of course,
> the huge advantage is that you can't use these functions to write buggy
> code (at least in the sense of breaking the static enforcement of patch
> ordering).


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

how to nicely implement phantom type coersion?

oleg-7
In reply to this post by David Roundy

David Roundy wrote:

] The basic idea is that a patch will have type (Patch a b) where "a" and "b"
] are phantom types.  Sequential patches will have identical ending and
] beginning types.  So that a sequential pair, for example, can be written as
]
] data Sequential a c where
]     Sequential :: Patch a b -> Patch b c -> Sequential a c
]
] The trickiness is that we need to be able to check for equality of two
] patches, and if they are truly equal, then we know that their ending states
] are also equal.  We do this with a couple of operators:
]
]     (=\/=) :: Patch a b -> Patch a c -> Maybe (EqContext b c)
]     (=/\=) :: Patch a z -> Patch b z -> Maybe (EqContext a b)
] data EqContext a b =
]     EqContext { coerce_start :: Patch a z -> Patch b z,
]                 coerce_end :: Patch z a -> Patch z b,
]                 backwards_coerce_start :: Patch b z -> Patch a z,
]                 backwards_coerce_end :: Patch z b -> Patch z a
]               }
]
] where we use the EqContext to encapsulate unsafeCoerce so that it can only
] be used safely.  The problem is that it's tedious figuring out whether to
] use coerce_start or coerce_end, or backwards_coerce_end, etc.

I'd like to remark first that unsafeCoerce isn't actually necessary
because the types to coerce to/from are phantom. If the data
constructor is available, we can always `coerce' from one type to the
other.

The data type EqContext seems to be overkill. As I understand it, the
problem is to be able to translate run-time equality of _values_ into
an evidence that can later be used to interconvert values of two
different _types_. As a side remark, such problems are often easier to
solve if we write in CPS style (cf. for example, the Implicit
Configurations paper). Anyway, the following code hopefully helps with
the problem at hand:


> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
>
> module P where

In the real patch, the content of a patch is probably a string or an
array of strings, or a file name. Integers should suffice here.

> data Patch a b = Patch Int -- Hide the constructor (except for class Coerce)
>       deriving Show

Suppose that our repository is in state S1 and we received a patch p1
(whose application takes the repository to state S2):

> -- Patch p1 is applied to state 1
> p1 :: Patch S1 S2 = Patch 1

We then received two patches p2 and p3 in parallel:

> -- Patches p2 and p3 are both received in State 2
> -- We don't know (yet) if they are the same though...
> p2 :: Patch S2 S3 = Patch 2
> p3 :: Patch S2 S4 = Patch 2 -- the same patch actually

We can compose patches like this:

> sequential :: Patch a b -> Patch b c -> Patch a c
> sequential (Patch x) (Patch y) = Patch (x+y)
>
> s1 = sequential p1 p2
> s2 = sequential p1 p3

 *P> :t s1
 s1 :: Patch S1 S3
 *P> :t s2
 s2 :: Patch S1 S4

The patches s1 and s2 are _intensionally_ the same but extensionally
different. Indeed, if we try to place them in a list, we fail

*> l1 = [s1,s2]

    Couldn't match `S3' against `S4'
      Expected type: Patch S1 S3
      Inferred type: Patch S1 S4
    In the list element: s2
    In the definition of `l1': l1 = [s1, s2]

There is hope however: creating a witness: EQP a b is a witness that
the types a and b are the same. The value of the witness is not important...

> data EQP a b = EQP -- Hide the constructor!

The following creates the proof:

> (=\/=) :: Patch a b -> Patch a c -> Maybe (EQP b c)
> Patch x =\/= Patch y = if x == y then Just EQP else Nothing
>
> (=/\=) :: Patch a z -> Patch b z -> Maybe (EQP a b)
> Patch x =/\= Patch y = if x == y then Just EQP else Nothing

We can now write

> test1 = cons s1 s2
>   where
>   cons s1 s2 | Just e <- p2 =\/= p3 = Just [s1, coerce s2 e]
>   cons _ _ = Nothing
>
> test2 = cons s1 s2
>   where
>   cons s1 s2 | Just e <- p2 =\/= p3 = Just [coerce s1 e, s2]
>   cons _ _ = Nothing
>
> p4 :: Patch S2 S5 = Patch 4
>
> test3 = cons s1 (sequential p1 p4)
>   where
>   cons s1 s2 | Just e <- p2 =\/= p4 = Just [coerce s1 e, s2]
>   cons _ _ = Nothing

  *P> test1
  Just [Patch 3,Patch 3]
  *P> test2
  Just [Patch 3,Patch 3]
  *P> test3
  Nothing

It should be stressed that we never had to worry if we have to coerce
the start type of Patch or the end type of Patch, forward or
backward. We just apply `coerce' (to whatever value) and the compiler
figures out the rest -- what to coerce to what.

The implementation

> class Coerce a b c d e f | a b c d -> e f where
>     coerce :: Patch a b -> EQP c d -> Patch e f
>     coerce (Patch x) _ = Patch x
>
> instance Coerce a b b c a c
>
> instance Coerce a b c b a c
>
> instance Coerce a b a c c b
>
> instance Coerce a b c a c b
>
>
> -- States of patching...
> data S1
> data S2
> data S3
> data S4
> data S5

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

Re: [darcs-conflicts] how to nicely implement phantom type coersion?

Jim Apple-2
In reply to this post by Ralf Hinze
Ralf Hinze wrote:
> the type a :=: b defined below
> goes back to  Leibniz's principle of substituting equals for equals:

If you like this, check out two of Ralf's papers:

First-class phantom types:
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2003-1901
Fun with phantom types:
http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf

The first (in section 2.4) explains a limitation of :=:

I highly recommend both papers.

Jim

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

Re: how to nicely implement phantom type coersion?

David Roundy
In reply to this post by Thomas Jaeger-3
On Thu, Dec 08, 2005 at 05:31:37PM -0500, Thomas Jger wrote:
> Since you're already using GADTs, why not also use them to witness type
> equality:

Thanks for the suggestion! This just illustrates the rule that when using
GADTs the solution to every problem is to introduce another GADT.  It
amazes me how many times that rule has proven true, and yet I *still* don't
think to define a new GADT for every problem I run into...
--
David Roundy
http://www.darcs.net
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe