Does this, and should this type check on GHC 6.10.x ?

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

Does this, and should this type check on GHC 6.10.x ?

Ahn, Ki Yung
Dear GHC type hackers,

We got a code (please refer to the attached lhs file) that uses type
families and type classes very cleverly.  We don't know who wrote
itbecause this was a contribution of an anonymous reviewer on our paper,
which we are still revising. http://kyagrd.dyndns.org/wiki/SharedSubtypes
Although we learned a lot from this code, we still have unsolved
question about this code.

The problem is, we are still not sure whether this code actually type
checks in any GHC version, and we are not even sure whether this should
type check or not as it is.  I wasn't able to type check this in any of
the GHC versions 6.10.1 on windows and debian linux, GHC 6.10.2 on
windows and debian linux, or GHC 6.10.3 on debian linux.  I also asked
some of my colleagues at my school who has GHC installed to run this
code, but they weren't able to load up either.

However, some people we email conversation with reported that they were
able to successfully load this code in GHC version 6.10.1 in their
system.  This is very surprising because we weren't able to type check
it with the same version (GHC 6.10.1) on our machines (Windows XP and
Debian Linux).  Since there is no reason that GHC type checker would
behave differently among different platforms, the code I am attaching is
still an unsolved misery to us.

It would be very helpful for us if any of can type check this successful
could report what version of GHC on what platform and what GHC command
line options used to make this code type check.  And also, we welcome
any discussion whether this code should or should not in principle type
check.

Thanks in advance,

Ahn, Ki Yung


FYI, I had the following error message when I tried it on ghc 6.10.3.
(When I commented out the problematic line, the last equation of crossB,
I was able to load it up though.  So, this code definitely doesn't seem
to be just thought out of one's mind without actually running on ghc.)

========================================================================

kyagrd@kyavaio:~/tmp$ ghci --version
The Glorious Glasgow Haskell Compilation System, version 6.10.3
kyagrd@kyavaio:~/tmp$ ghci -fglasgow-exts -XUndecidableInstances
Review3.lhs
GHCi, version 6.10.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Main             ( Review3.lhs, interpreted )

Review3.lhs:67:29:
    Could not deduce (Expandable (Tuple (Map ((,) t2) ys)))
      from the context (xs ~ t2 ::: ts2, Expandable t2)
      arising from a use of `:::' at Review3.lhs:67:29-59
    Possible fix:
      add (Expandable (Tuple (Map ((,) t2) ys))) to the context of
        the constructor `:::'
      or add an instance declaration for
         (Expandable (Tuple (Map ((,) t2) ys)))
    In the expression: Bs (mapB x ys) ::: crossB xs ys
    In the definition of `crossB':
        crossB (x ::: xs) ys = Bs (mapB x ys) ::: crossB xs ys
    In the definition of `expandPair':
        expandPair _ pair (a ::: as) (b ::: bs)
                     = crossB (a ::: as) (b ::: bs)
                     where
                         crossB :: BList xs -> BList ys -> BList (Cross
xs ys)
                         crossB Nil ys = Nil
                         crossB (x ::: xs) ys = Bs (mapB x ys) :::
crossB xs ys
                         mapB ::
                           (Expandable x) => Bit x -> BList ys -> BList
(Map ((,) x) ys)
                         mapB x Nil = Nil
                         mapB x (y ::: ys) = pair x y ::: mapB x ys
Failed, modules loaded: none.


-------------------- review 3 --------------------

PAPER: 8
TITLE: Functional Pearl: Sparse Bitmaps for Pattern Match Coverage
 
OVERALL RATING: -2 (strong reject)
REVIEWER'S CONFIDENCE: 4 (expert)
Novelty: 2 (Average)

----------------------- REVIEW --------------------

The paper describes an algorithm for checking pattern match coverage using
expandable bit masks. The first half of the paper describes a simply typed
version where the types of the pattern are represented as data being passed
around. This part is quite good.
However, in the second half of the paper a failed attempt is made at reflecting
the types of the patterns as Haskell types, allowing matching against
polymorphic patterns. This implementation is poorly explained and it seems like
the authors haven't fully understood why it isn't working. In fact, it is quite
possible to make it work (see below).
This could be a very nice paper if the second half were rewritten.
Making it work:

> type family   Expand t
> type instance Expand ()         = Nil
> type instance Expand (a, b)     = ExpandPair (Expand a) (Expand b)
> type instance Expand Bool       = () ::: () ::: Nil
> type instance Expand (Maybe a)  = () ::: a ::: Nil
> type instance Expand [a]        = () ::: (a, [a]) ::: Nil
> type instance Expand (Tuple xs) = xs
> type family   ExpandPair as bs
> type instance ExpandPair as         Nil        = as
> type instance ExpandPair Nil        (b ::: bs) = b ::: bs
> type instance ExpandPair (a ::: as) (b ::: bs) = Cross (a ::: as) (b ::: bs)
> type family   Cross as bs
> type instance Cross Nil        bs = Nil
> type instance Cross (a ::: as) bs = Tuple (Map ((,) a) bs) ::: Cross as bs
> type family   Map (f :: * -> *) xs
> type instance Map f Nil        = Nil
> type instance Map f (x ::: xs) = f x ::: Map f xs
> data Tuple xs
> data Bit t where
>   O  :: Bit t
>   I  :: Expandable t => Bit t
>   Bs :: BList (Expand t) -> Bit t
> data Nil
> data x ::: xs
> data BList ts where
>   Nil   :: BList Nil
>   (:::) :: Expandable t => Bit t -> BList ts -> BList (t ::: ts)
> class Expandable t where
>   expand :: Bit t -> BList (Expand t)
> instance (Expandable a, Expandable b) => Expandable (a, b) where
>   expand (I :: Bit (a, b)) =
>     expandPair (undefined :: (a, b))
>                (\_ _ -> I) (expand (I :: Bit a)) (expand (I :: Bit b))
> expandPair :: forall a b. (Expandable a, Expandable b) =>
>               (a, b) -> -- for unification purposes
>               (forall x y. (Expandable x, Expandable y) => Bit x -> Bit y -> Bit (x, y)) ->
>               BList (Expand a) -> BList (Expand b) -> BList (Expand (a, b))
> expandPair _ pair as         Nil        = as
> expandPair _ pair Nil        (b ::: bs) = b ::: bs
> expandPair _ pair (a ::: as) (b ::: bs) = crossB (a ::: as) (b ::: bs)
>   where
>     crossB :: BList xs -> BList ys -> BList (Cross xs ys)
>     crossB Nil        ys = Nil
>     crossB (x ::: xs) ys = Bs (mapB x ys) ::: crossB xs ys
>     mapB :: Expandable x => Bit x -> BList ys -> BList (Map ((,) x) ys)
>     mapB x Nil        = Nil
>     mapB x (y ::: ys) = pair x y ::: mapB x ys
> (|*|) :: forall t u. (Expandable t, Expandable u) => Bit t -> Bit u -> Bit (t, u)
> O     |*| _     = O
> _     |*| O     = O
> I     |*| I     = I
> I     |*| Bs ys = case expand (I :: Bit t) of
>                     Nil -> Bs (cast ys)
>                     xs  -> Bs xs |*| Bs ys
>   where
>     cast :: BList bs -> BList (ExpandPair Nil bs)
>     cast Nil        = Nil
>     cast (b ::: bs) = b ::: bs
> Bs xs |*| I     = case expand (I :: Bit u) of
>                     Nil -> Bs xs
>                     ys  -> Bs xs |*| Bs ys
> Bs xs |*| Bs ys = Bs (expandPair (undefined :: (t, u)) (|*|) xs ys)


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

Re: Does this, and should this type check on GHC 6.10.x ?

Brandon S Allbery KF8NH
On Jun 26, 2009, at 00:47 , Ahn, Ki Yung wrote:
We got a code (please refer to the attached lhs file) that uses type
families and type classes very cleverly.  We don't know who wrote

I'm under the impression that many clever uses of type families require GHC HEAD, as they're still evolving.

-- 
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] [hidden email]
system administrator [openafs,heimdal,too many hats] [hidden email]
electrical and computer engineering, carnegie mellon university    KF8NH



_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

PGP.sig (202 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Does this, and should this type check on GHC 6.10.x ?

Tom Schrijvers-2
In reply to this post by Ahn, Ki Yung
> We got a code (please refer to the attached lhs file) that uses type
> families and type classes very cleverly.  We don't know who wrote
> itbecause this was a contribution of an anonymous reviewer on our paper,
> which we are still revising. http://kyagrd.dyndns.org/wiki/SharedSubtypes
> Although we learned a lot from this code, we still have unsolved
> question about this code.
>
> The problem is, we are still not sure whether this code actually type
> checks in any GHC version, and we are not even sure whether this should
> type check or not as it is.

Have you first, before you turn to GHC< considered whether this code
should be well-typed in any type system?

> Review3.lhs:67:29:
>    Could not deduce (Expandable (Tuple (Map ((,) t2) ys)))
>      from the context (xs ~ t2 ::: ts2, Expandable t2)
>      arising from a use of `:::' at Review3.lhs:67:29-59

At first sight, it looks like this constraint

  Expandable (Tuple (Map ((,) t2) ys))
is indeed one that's required to hold in order to make the code
well-typed. Do you agree?

Yet I see no instance of Expandable for Tuple. So why do you think this
constraint should hold anyway?

Tom


--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: [hidden email]
url: http://www.cs.kuleuven.be/~toms/

Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Does this, and should this type check on GHC 6.10.x ?

Ahn, Ki Yung
In reply to this post by Ahn, Ki Yung
Tom Schrijvers wrote:

>
> Have you first, before you turn to GHC< considered whether this code
> should be well-typed in any type system?
>
>> Review3.lhs:67:29:
>>    Could not deduce (Expandable (Tuple (Map ((,) t2) ys)))
>>      from the context (xs ~ t2 ::: ts2, Expandable t2)
>>      arising from a use of `:::' at Review3.lhs:67:29-59
>
> At first sight, it looks like this constraint
>
>     Expandable (Tuple (Map ((,) t2) ys))
> is indeed one that's required to hold in order to make the code
> well-typed. Do you agree?
>
 > Yet I see no instance of Expandable for Tuple. So why do you
 > think this constraint should hold anyway?

I agree with you.  I think the code is not supposed to type check, and
that's what I experience from GHC so far.

One problem that bothers us is that, as I mentioned in my original
message, there were at least two reports that they were possible to type
check in GHC, which we cannot reproduce.  So, I'm just wondering what
version and settings that makes it type check (if such version or
setting exists, its good for GHC type system developers to be aware of
it), and just double check if there is any other typing rules/theories
that I am not aware of makes the code type check (if such version of GHC
exists and it is not a bug).

Another problem, which I haven't mentioned, I have when I tried to make
additional type family instance declarations  that latest (stable)
distributions of GHC 6.10.x does not let me declare instances of
(Expandable (Tuple (Map ((,) t2) ys))).  When you try declaring such an
instance something like this:

 > instance Expandable (Tuple (Map ((,) t2) ys)) where
 > ...

GHC will give me an error message that type synonyms are not allowed in
instance declarations:
kyagrd@kyavaio:~/tmp$ ghci -fglasgow-exts -XUndecidableInstances
Review3.lhs
GHCi, version 6.10.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Main             ( Review3.lhs, interpreted )

Review3.lhs:62:2:
     Illegal type synonym family application in instance:
         Tuple (Map ((,) t2) ys)
     In the instance declaration for `Expandable (Tuple (Map ((,) t2) ys))'
Failed, modules loaded: none.

So, my impression is that there is little hope even I try fixing this by
adding more instance declarations, even if this was an incomplete code
because of space restrictions of the review.  But I still wanted to
double check and discuss this matter with mailing list readers since
there were few reports (which we fail to reproduce) that this type
checks in their installation of GHC.

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

Re: Does this, and should this type check on GHC 6.10.x ?

Ahn, Ki Yung
Ahn, Ki Yung wrote:
>
> Another problem, which I haven't mentioned, I have when I tried to make
> additional type family instance declarations  that latest (stable)

Typo: I mean type class instance declaration of course.

> distributions of GHC 6.10.x does not let me declare instances of
> (Expandable (Tuple (Map ((,) t2) ys))).  When you try declaring such an
> instance something like this:
>
>  > instance Expandable (Tuple (Map ((,) t2) ys)) where
>  > ...
>
> GHC will give me an error message that type synonyms are not allowed in
> instance declarations:
> kyagrd@kyavaio:~/tmp$ ghci -fglasgow-exts -XUndecidableInstances
> Review3.lhs
> GHCi, version 6.10.3: http://www.haskell.org/ghc/  :? for help
> Loading package ghc-prim ... linking ... done.
> Loading package integer ... linking ... done.
> Loading package base ... linking ... done.
> [1 of 1] Compiling Main             ( Review3.lhs, interpreted )
>
> Review3.lhs:62:2:
>     Illegal type synonym family application in instance:
>         Tuple (Map ((,) t2) ys)
>     In the instance declaration for `Expandable (Tuple (Map ((,) t2) ys))'
> Failed, modules loaded: none.
>
> So, my impression is that there is little hope even I try fixing this by
> adding more instance declarations, even if this was an incomplete code
> because of space restrictions of the review.  But I still wanted to
> double check and discuss this matter with mailing list readers since
> there were few reports (which we fail to reproduce) that this type
> checks in their installation of GHC.

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users