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.