[Haskell-cafe] Need help understanding a GADT related error

Mon Feb 18 13:35:47 UTC 2019

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.
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20190218/b792b8ad/attachment.sig>