Re: [Haskell-cafe] MPTC and quantification in GADTs vs. regular ADTs

11 Apr 2016

      If you change latter definition to

data T row col
    = MPTC row col =>
      T { col :: col
        , row :: row }

I.e. remove `forall row col`, then everything starts to work. As your definition is (with unique names) is:

data T anyrow anycol
    = forall row col. MPTC row col =>
      T { col :: col
        , row :: row }

i.e. the indexes are phantom and field types are existential.

In the first version, the `forall row col` is harmless, as the indexes are repeated in GADT syntax: -> T row col

- Oleg
...
On 11 Apr 2016, at 10:57, Kosyrev Serge <_deepfire@feelingofgreen.ru> wrote:
Good day folks!
What is the explanation for the difference in GHC reaction towards the
two variants of the following piece of code:
...
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UnicodeSyntax #-}
import Prelude.Unicode
class MPTC row col where
class TC a where
   method ∷ a → a
1 data T row col where
1      T ∷ ∀ row col. MPTC row col ⇒
1          { col ∷ col
1          , row ∷ row } → T row col
2 data T row col
2     = ∀ row col. MPTC row col ⇒
2       T { col ∷ col
2         , row ∷ row }
...
instance MPTC row col ⇒ TC (T row col) where
   method w@T{..} =
       seq (recover (toCol w) row) w
toCol ∷ MPTC row col ⇒ T row col → col
toCol = (⊥)
recover ∷ MPTC row col ⇒ col → row → T row col
recover = T
Note the missing
...
instance MPTC row col
Nevertheless, the former typechecks, while the latter is rejected with:
...
mptc-data-vs-gadt.hs:23:14-34: error: …
   • Could not deduce (MPTC row1 col) arising from a use of ‘recover’
     from the context: MPTC row col
       bound by the instance declaration
       at mptc-data-vs-gadt.hs:21:10-38
     or from: MPTC row1 col1
       bound by a pattern with constructor:
                  T :: forall row col row col.
                       MPTC row col =>
                       col -> row -> T row col,
                in an equation for ‘method’
       at mptc-data-vs-gadt.hs:22:14-18
     Possible fix:
       add (MPTC row1 col) to the context of the data constructor ‘T’
   • In the expression: (recover (toCol w) row)
     In the expression: seq (recover (toCol w) row) w
     In an equation for ‘method’:
         method w@(T {..}) = seq (recover (toCol w) row) w
I'm sure this must have something to do with GADTs carrying type
equality constraints, but still I don't quite understand the difference
in interpretation of the forall quantification.
To my understanding, a value bound by the pattern 'w@T{..}' ought to be
treated as sufficient evidence for 'MPTC row col', no matter whether
it is a GADT or not.
..but it isn't.
--
с уважениeм / respectfully,
Косырев Сергей
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] MPTC and quantification in GADTs vs. regular ADTs

Oleg Grenrus