Need help understanding a GADT related error

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

Need help understanding a GADT related error

Hilco Wijbenga
Hi all,

I created some GADT code (see https://pastebin.com/vkJ3RzNA and
below). When compiling this I get these errors:

$ stack build
parser-0.1.0.0: build (exe)
Preprocessing executable 'parser' for parser-0.1.0.0..
Building executable 'parser' for parser-0.1.0.0..
[2 of 2] Compiling Main             ( src/Main.hs,
.stack-work/dist/x86_64-linux-tinfo6/Cabal-2.2.0.1/build/parser/parser-tmp/Main.o
)

/home/hilco/workspaces/haskell/parser/src/Main.hs:30:18: error:
   • Couldn't match type ‘a’ with ‘E’
     ‘a’ is a rigid type variable bound by
       the type signature for:
         h :: forall a. H (T a)
       at src/Main.hs:29:1-12
     Expected type: T a
       Actual type: T E
   • In the expression: E' (E "E")
     In the expression: (E' (E "E"), [])
     In an equation for ‘h’: h [] = (E' (E "E"), [])
   • Relevant bindings include
       h :: H (T a) (bound at src/Main.hs:30:1)
  |
30 | h []          = (E' (E "E"), [])
  |                  ^^^^^^^^^^

/home/hilco/workspaces/haskell/parser/src/Main.hs:34:16: error:
   • Couldn't match type ‘B’ with ‘A’
     Expected type: P Char (T A)
       Actual type: P Char (T B)
   • In the expression: b
     In the second argument of ‘tt’, namely ‘[a, b]’
     In the expression: tt h [a, b]
  |
34 | tt' = tt h [a, b]
  |                ^

--  While building custom Setup.hs for package parser-0.1.0.0 using:
     /home/hilco/.stack/setup-exe-cache/x86_64-linux-tinfo6/Cabal-simple_mPHDZzAJ_2.2.0.1_ghc-8.4.3
--builddir=.stack-work/dist/x86_64-linux-tinfo6/Cabal-2.2.0.1 build
exe:parser --ghc-options " -ddump-hi -ddump-to-file
-fdiagnostics-color=always"
   Process exited with code: ExitFailure 1

Why is "T a" not a more generic version of "T E"? Why doesn't "T E + T
A + TB" yield "T a" as a generic type?

Cheers,
Hilco

 1 {-# LANGUAGE GADTs #-}
 2
 3 module Main where
 4
 5 data PR t a = PR (Maybe ([t], a))
 6 data P  t a = P  ([t] -> PR t a)
 7
 8 a :: P Char (T A)
 9 a = undefined
10
11 b :: P Char (T B)
12 b = undefined
13
14 data A = A
15 data B = B
16 data E = E String
17
18 data T a where
19     A' :: T A
20     B' :: T B
21     E' :: E -> T E
22
23 type H t = [Char] -> (t, [Char])
24 type TT t = [Char] -> [t]
25
26 tt :: H t -> [P Char t] -> TT t
27 tt = undefined
28
29 h :: H (T a)
30 h []          = (E' (E "E"), [])
31 h (head:rest) = (E' (E ("E")), rest)
32
33 tt' :: [Char] -> [T a]
34 tt' = tt h [a, b]
35
36 main :: IO ()
37 main = putStrLn "Hello"
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Need help understanding a GADT related error

Sven Bartscher
Hi Hilco,

Am 18.02.19 um 06:20 schrieb Hilco Wijbenga:

> Hi all,
>
> I created some GADT code (see https://pastebin.com/vkJ3RzNA and
> below). When compiling this I get these errors:
>
> $ stack build
> parser-0.1.0.0: build (exe)
> Preprocessing executable 'parser' for parser-0.1.0.0..
> Building executable 'parser' for parser-0.1.0.0..
> [2 of 2] Compiling Main             ( src/Main.hs,
> .stack-work/dist/x86_64-linux-tinfo6/Cabal-2.2.0.1/build/parser/parser-tmp/Main.o
> )
>
> /home/hilco/workspaces/haskell/parser/src/Main.hs:30:18: error:
>    • Couldn't match type ‘a’ with ‘E’
>      ‘a’ is a rigid type variable bound by
>        the type signature for:
>          h :: forall a. H (T a)
>        at src/Main.hs:29:1-12
>      Expected type: T a
>        Actual type: T E
>    • In the expression: E' (E "E")
>      In the expression: (E' (E "E"), [])
>      In an equation for ‘h’: h [] = (E' (E "E"), [])
>    • Relevant bindings include
>        h :: H (T a) (bound at src/Main.hs:30:1)
>   |
> 30 | h []          = (E' (E "E"), [])
>   |                  ^^^^^^^^^^
>
> /home/hilco/workspaces/haskell/parser/src/Main.hs:34:16: error:
>    • Couldn't match type ‘B’ with ‘A’
>      Expected type: P Char (T A)
>        Actual type: P Char (T B)
>    • In the expression: b
>      In the second argument of ‘tt’, namely ‘[a, b]’
>      In the expression: tt h [a, b]
>   |
> 34 | tt' = tt h [a, b]
>   |                ^
>
> --  While building custom Setup.hs for package parser-0.1.0.0 using:
>      /home/hilco/.stack/setup-exe-cache/x86_64-linux-tinfo6/Cabal-simple_mPHDZzAJ_2.2.0.1_ghc-8.4.3
> --builddir=.stack-work/dist/x86_64-linux-tinfo6/Cabal-2.2.0.1 build
> exe:parser --ghc-options " -ddump-hi -ddump-to-file
> -fdiagnostics-color=always"
>    Process exited with code: ExitFailure 1
>
> Why is "T a" not a more generic version of "T E"? Why doesn't "T E + T
> A + TB" yield "T a" as a generic type?
I'm pretty sure I'm using the wrong terminology for this, but I would
describe this as a problem of the “direction” of the generality. When
you give `h` a type of `[Char] -> (T a, [Char])`, you say that the
caller of `h` gets to decide for what type `a` will be.

In your implementation the value returned by `h` always has the type `(T
E, [Char])`, but your type promises that it is also able to be `(T Char,
[Char])`, `(T Int, [Char])` or whatever the caller wants the returned
value to be. The actually returned value of type `(T E, [Char])` is thus
too special to fulfil the general promise of `(T a, [Char])`.

Your second error is similar in concept, but has the added complexity,
that you try to put two values of different types (`a :: P Char (T A)`
and `b :: P Char (T B)`) into a list. When you put values together into
a list of type `[e]`, then that `e` is instantiated to be exactly *one*
type and all values in the list have to have exactly that type.

When the user of a value of type `a` gets to decide what concrete type
that value will have, the type variable `a` is called “universally
quantified”. When, as in your case, the supplier of the value gets do
decide what concrete type `a` will be, `a` is called “existentially
quantified”, but Haskell doesn't generally support existentially
quantified type variables.

Haskell does have an extension called ExistentialQuantification that
allows you to define data types that have type variables “inside” that
can not be seen from the outside, which is like having an existentially
quantified variable. I think this might be a solution to you problem,
though I don't think I understand the design of your code well enough to
suggest a definitive course of action here. You can read up on
ExistentialQuantification at [1].

Regards
Sven

[1]: https://wiki.haskell.org/Existential_type

>  1 {-# LANGUAGE GADTs #-}
>  2
>  3 module Main where
>  4
>  5 data PR t a = PR (Maybe ([t], a))
>  6 data P  t a = P  ([t] -> PR t a)
>  7
>  8 a :: P Char (T A)
>  9 a = undefined
> 10
> 11 b :: P Char (T B)
> 12 b = undefined
> 13
> 14 data A = A
> 15 data B = B
> 16 data E = E String
> 17
> 18 data T a where
> 19     A' :: T A
> 20     B' :: T B
> 21     E' :: E -> T E
> 22
> 23 type H t = [Char] -> (t, [Char])
> 24 type TT t = [Char] -> [t]
> 25
> 26 tt :: H t -> [P Char t] -> TT t
> 27 tt = undefined
> 28
> 29 h :: H (T a)
> 30 h []          = (E' (E "E"), [])
> 31 h (head:rest) = (E' (E ("E")), rest)
> 32
> 33 tt' :: [Char] -> [T a]
> 34 tt' = tt h [a, b]
> 35
> 36 main :: IO ()
> 37 main = putStrLn "Hello"
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
>

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

signature.asc (849 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Need help understanding a GADT related error

Brandon Allbery
In reply to this post by Hilco Wijbenga
This doesn't look like GADT related, just a common misunderstanding of how types work.

"h :: H (T a)" means the *caller* determines what type 'a will be, and "h" will work with that type. But "h" is instead using its own specific 'a.

On Mon, Feb 18, 2019 at 12:22 AM Hilco Wijbenga <[hidden email]> wrote:
Hi all,

I created some GADT code (see https://pastebin.com/vkJ3RzNA and
below). When compiling this I get these errors:

$ stack build
parser-0.1.0.0: build (exe)
Preprocessing executable 'parser' for parser-0.1.0.0..
Building executable 'parser' for parser-0.1.0.0..
[2 of 2] Compiling Main             ( src/Main.hs,
.stack-work/dist/x86_64-linux-tinfo6/Cabal-2.2.0.1/build/parser/parser-tmp/Main.o
)

/home/hilco/workspaces/haskell/parser/src/Main.hs:30:18: error:
   • Couldn't match type ‘a’ with ‘E’
     ‘a’ is a rigid type variable bound by
       the type signature for:
         h :: forall a. H (T a)
       at src/Main.hs:29:1-12
     Expected type: T a
       Actual type: T E
   • In the expression: E' (E "E")
     In the expression: (E' (E "E"), [])
     In an equation for ‘h’: h [] = (E' (E "E"), [])
   • Relevant bindings include
       h :: H (T a) (bound at src/Main.hs:30:1)
  |
30 | h []          = (E' (E "E"), [])
  |                  ^^^^^^^^^^

/home/hilco/workspaces/haskell/parser/src/Main.hs:34:16: error:
   • Couldn't match type ‘B’ with ‘A’
     Expected type: P Char (T A)
       Actual type: P Char (T B)
   • In the expression: b
     In the second argument of ‘tt’, namely ‘[a, b]’
     In the expression: tt h [a, b]
  |
34 | tt' = tt h [a, b]
  |                ^

--  While building custom Setup.hs for package parser-0.1.0.0 using:
     /home/hilco/.stack/setup-exe-cache/x86_64-linux-tinfo6/Cabal-simple_mPHDZzAJ_2.2.0.1_ghc-8.4.3
--builddir=.stack-work/dist/x86_64-linux-tinfo6/Cabal-2.2.0.1 build
exe:parser --ghc-options " -ddump-hi -ddump-to-file
-fdiagnostics-color=always"
   Process exited with code: ExitFailure 1

Why is "T a" not a more generic version of "T E"? Why doesn't "T E + T
A + TB" yield "T a" as a generic type?

Cheers,
Hilco

 1 {-# LANGUAGE GADTs #-}
 2
 3 module Main where
 4
 5 data PR t a = PR (Maybe ([t], a))
 6 data P  t a = P  ([t] -> PR t a)
 7
 8 a :: P Char (T A)
 9 a = undefined
10
11 b :: P Char (T B)
12 b = undefined
13
14 data A = A
15 data B = B
16 data E = E String
17
18 data T a where
19     A' :: T A
20     B' :: T B
21     E' :: E -> T E
22
23 type H t = [Char] -> (t, [Char])
24 type TT t = [Char] -> [t]
25
26 tt :: H t -> [P Char t] -> TT t
27 tt = undefined
28
29 h :: H (T a)
30 h []          = (E' (E "E"), [])
31 h (head:rest) = (E' (E ("E")), rest)
32
33 tt' :: [Char] -> [T a]
34 tt' = tt h [a, b]
35
36 main :: IO ()
37 main = putStrLn "Hello"
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


--
brandon s allbery kf8nh

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Need help understanding a GADT related error

David Banas-2
In reply to this post by Hilco Wijbenga
Hilco,

Your first error arrises, because you’re offering to the caller of `h` that she may demand any type of `a`, but are “hard-wiring” `a :: T E` in the definition of that function. Reflecting that fact in the function type signature eliminates the error:

-- h :: H (T a)
h :: H (T E)
h []          = (E' (E "E"), [])
h (head:rest) = (E' (E ("E")), rest)

Your second error is explained (I hope) in the comments I’ve added to your original code:

tt' :: [Char] -> [T a]
tt' = tt h [a, b]
-- tt :: H t -> [P Char t] -> TT t
--    :: ([Char] -> (t, [Char])) -> [P Char t] -> [Char] -> [t]
--
-- h :: [Char] -> (t, [Char]) ~ H (T E)
-- h :: [Char] -> (t, [Char]) ~ [Char] -> (T E, [Char])
-- ==> t ~ T E
--
-- [a, b] :: [P Char t]
-- a      :: P Char (T E) /~ P Char (T A)
-- b      :: P Char (T E) /~ P Char (T B)

-db



_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.