[Haskell-cafe] Type equality with "forall"
Tom Murphy
amindfv at gmail.com
Wed Mar 9 19:30:11 UTC 2016
Thanks for the reply, Adam!
It looks like the problem is the combination of existentials and
overlapping instances (which don't behave sensibly together).
Here's a new version (that also doesn't work!) but that I think is a lot
closer -- this one uses type families instead of overlapping instances:
[pragmas [0]]
import Data.Proxy
-- Same as before:
data Fs a c where
F :: (a -> c) -> Fs a c
Compose :: forall a b c. Fs b c -> Fs a b -> Fs a c
class TEq x0 x1 y0 y1 where
isEq :: Fs x0 x1 -> (y0 -> y1) -> String
instance (
flag ~ IEq (Fs x0 x1) (y0 -> y1)
, TEq' x0 x1 y0 y1 flag
) => TEq x0 x1 y0 y1 where
isEq = isEq' (Proxy::Proxy flag)
type family IEq a b :: Bool where
IEq (Fs x0 x1) (xo -> x1) = 'True
IEq a b = 'False
class TEq' x0 x1 y0 y1 (flag :: Bool) where
isEq' :: Proxy flag -> (Fs x0 x1) -> (y0 -> y1) -> String
instance TEq' x0 x1 y0 y1 'True where
isEq' _ _ _ = "yes!"
instance TEq' x0 x1 y0 y1 'False where
isEq' _ (F _) _ = "no"
-- isEq' _ (Compose a b) f = "compose("++isEq a f++", "++isEq b f++")"
The problem is the last line -- the "hidden" type can't be inferred to be
in TEq', although every type is in fact in TEq'
Any more help would be very appreciated!
Thanks,
Tom
[0]
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs, NoMonoLocalBinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-} -- new
{-# LANGUAGE TypeFamilies #-} -- new
{-# LANGUAGE UndecidableInstances #-}
On Wed, Mar 9, 2016 at 1:51 PM, adam vogt <vogt.adam at gmail.com> wrote:
> Hi Tom,
>
> It looks like after a type variable is hidden (existentially quantified is
> probably the term), you don't get it back to pick the more specific
> instance. Here's a shorter example than yours:
>
> {-# LANGUAGE FlexibleInstances, GADTs #-}
>
> class C a where c :: a -> String
>
> instance {-# OVERLAPPABLE #-} C a where c _ = "fallback"
> instance {-# OVERLAPS #-} C Char where c _ = "char"
>
> data T where T :: a -> T
>
> example = case T 'x' of T x -> c x
> -- prints "fallback"
>
> In this example you can change the T constructor to T :: C a => a -> T to
> get "char" printed, but I can't figure the equivalent of that for your
> class. The closest I can get is to store the Typeable dictionary with the
> Compose constructor <http://lpaste.net/9086245683987480576> which would
> let you return "yes" when the wrong instance is chosen. But then if you
> have Typeable you probably don't need overlapping instances.
>
> Regards,
> Adam
>
>
> On Wed, Mar 9, 2016 at 12:21 PM, Tom Murphy <amindfv at gmail.com> wrote:
>
>> So I've written a library I'm pretty excited about, and there's just one
>> type issue keeping it from all working!
>>
>> I've got a graph that represents functions and function composition, and
>> I've written a class (pretty directly from Oleg's "TypeEq" work [0]) that
>> tells whether two types are equal. The problem is it doesn't always say
>> they're equal.
>>
>> Here's a simplified version that has the same issue:
>>
>>
>> [pragmas [1]]
>>
>> data Fs a c where
>> F :: (a -> c) -> Fs a c
>> Compose :: forall a b c. Fs b c -> Fs a b -> Fs a c
>>
>> -- Type equality:
>> class TEq x0 x1 y0 y1 (b :: Bool) | x0 x1 y0 y1 -> b where
>> isEq :: Fs x0 x1 -> (y0 -> y1) -> String
>>
>> -- The case where the types are equal:
>> instance {-# OVERLAPS #-} TEq x y x y 'True where
>> isEq _ _ = "yes!"
>>
>> -- The case where they're unequal:
>> instance (b ~ 'False) => TEq x0 x1 y0 y1 b where
>> isEq (F _) = "no"
>> isEq (Compose a b) f = "compose("++isEq a f++", "++isEq b f++")"
>>
>>
>>
>>
>>
>> When I try this on example programs, I see weird results:
>>
>> > isEq (F not) not
>> "yes!" -- expected
>> > isEq (Compose (F (\_->"")) (F not)) not
>> "compose(no, no)" -- weird!
>>
>> I would expect the result of the second one to be "compose(no, yes!)".
>>
>> It seems to think that the (F not) in the Compose has a different type
>> than (F not) not in a Compose.
>>
>> Anyone spot my problem?
>>
>> Thanks!
>> Tom
>>
>> [0] http://okmij.org/ftp/Haskell/typeEQ.html
>> [1]
>> {-# LANGUAGE DataKinds #-}
>> {-# LANGUAGE FlexibleInstances #-}
>> {-# LANGUAGE FunctionalDependencies #-}
>> {-# LANGUAGE GADTs, NoMonoLocalBinds #-}
>> {-# LANGUAGE KindSignatures #-}
>> {-# LANGUAGE MultiParamTypeClasses #-}
>> {-# LANGUAGE Rank2Types #-}
>> {-# LANGUAGE UndecidableInstances #-}
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160309/bc0cab36/attachment.html>
More information about the Haskell-Cafe
mailing list