Hi, I have a problem I cannot solve. I have a data type that I need to be readable, and the read instance derivable. I need it readable because it is going to be a data type for configuring at run time an application, and I want the application to read it when booting up. On the other side, I also need an existential type to be used within this data type: it is a list that must be polymorphic somehow. Since instances for existentially qualified types cannot be derived I thought to create a type that could be easily read. But I'm not able to write the parser, and I'm not sure if this is my fault or just a limitation I'm trying to futilely overcome. Below there's a piece of code that shows the problem. I'd like to be able to use MT to build a list like: [MT (T1a,1), MT (T1b,3)] And I'd like to read str with: read $ show str No way, and the code below compiles. Substituting return (m) with return (MT m) leads to error messages like: Ambiguous type variable `e' in the constraints What am I getting wrong? Is just the parser or there's something deeper? Thanks for your kind attention. All the best Andrea the code: ---------------------------------------------------------------- {-# OPTIONS -fglasgow-exts #-} module Test where import Text.Read import Text.ParserCombinators.ReadPrec data MyData = MD { rec1 :: String , rec2 :: String , rec3 :: [MyType] } deriving (Read,Show) data MyType = forall e . (MyClass e, Show e, Read e) => MT (e,Int) instance Show MyType where show (MT a) = "MT " ++ show a class MyClass c where myShow :: c -> String data TipoA = T1a | T2a | T3a deriving(Show,Read,Eq) instance MyClass TipoA where myShow T1a = "t1a" myShow T2a = "t2a" myShow T3a = "t3a" data TipoB = T1b | T2b | T3b deriving(Show,Read,Eq) instance MyClass TipoB where myShow T1b = "t1b" myShow T2b = "t2b" myShow T3b = "t3b" str :: MyData str = MD {rec1 = "Ciao", rec2 = "Ciao Ciao", rec3 = [MT (T1a,1), MT (T1b,3)] } instance Read MyType where readPrec = readMT readMT :: ReadPrec MyType readMT = prec 10 $ do Ident "MT" <- lexP parens $ do m <- readPrec return (m)
I'd like to be able to use MT to build a list like: [MT (T1a,1), MT (T1b,3)] And I'd like to read str with: read $ show str
Substituting return (m) with return (MT m) leads to error messages like: Ambiguous type variable `e' in the constraints
which is the important hint! the parser used for 'read' depends on the return type, but the existential type _hides_ the internal type which would be needed to select a read parser.
readMT :: ReadPrec MyType readMT = prec 10 $ do Ident "MT" <- lexP parens $ do m <- readPrec return (m)
if your hidden types have distinguishable 'show'-representations, you could write your own typecase like this (making use of the fact that 'read' parsers with incorrect type will fail, and that the internal type can be hidden after parsing) readMT :: ReadPrec MyType readMT = prec 10 $ do Ident "MT" <- lexP parens $ (do { m <- readPrec; return (MT (m::(TipoA,Int))) }) `mplus` (do { m <- readPrec; return (MT (m::(TipoB,Int))) }) *Test> read (show [MT (T1a,1),MT (T1b,3)]) :: [MyType] [MT (T1a,1),MT (T1b,3)] (if necessary, you could have 'show' embed a type representation for the hidden type, and dispatch on that representation in 'read') claus
On Mon, Jul 09, 2007 at 04:28:43PM +0100, Claus Reinke wrote:
which is the important hint! the parser used for 'read' depends on the return type, but the existential type _hides_ the internal type which would be needed to select a read parser.
I think that this is precisely what I wasn't getting. If I understand it correctly, this also means that what I supposed to be my smart trick is actually dumbly useless - the "Read e" here: forall e . (MyClass e, Show e, Read e) => MT (e,Int)
if your hidden types have distinguishable 'show'-representations, you could write your own typecase like this (making use of the fact that 'read' parsers with incorrect type will fail, and that the internal type can be hidden after parsing)
readMT :: ReadPrec MyType readMT = prec 10 $ do Ident "MT" <- lexP parens $ (do { m <- readPrec; return (MT (m::(TipoA,Int))) }) `mplus` (do { m <- readPrec; return (MT (m::(TipoB,Int))) })
*Test> read (show [MT (T1a,1),MT (T1b,3)]) :: [MyType] [MT (T1a,1),MT (T1b,3)]
(if necessary, you could have 'show' embed a type representation for the hidden type, and dispatch on that representation in 'read')
The problem is that I was trying to find a way to define the class (MyClass) and not writing a parser for every possible type (or even using their show-representation): I wanted a polymorphic list of types over which I could use the method defined for their class, but, as far as I can get it, this is not possible. Thanks for your kind attention. All the best, Andrea
which is the important hint! the parser used for 'read' depends on the return type, but the existential type _hides_ the internal type which would be needed to select a read parser.
forall e . (MyClass e, Show e, Read e) => MT (e,Int)
the 'Read' there ensures that we only inject types that have a reader, but it doesn't help us select one of the many possible types which have such a reader.
readMT :: ReadPrec MyType readMT = prec 10 $ do Ident "MT" <- lexP parens $ (do { m <- readPrec; return (MT (m::(TipoA,Int))) }) `mplus` (do { m <- readPrec; return (MT (m::(TipoB,Int))) })
The problem is that I was trying to find a way to define the class (MyClass) and not writing a parser for every possible type (or even using their show-representation): I wanted a polymorphic list of types over which I could use the method defined for their class, but, as far as I can get it, this is not possible.
i'm not sure i understand the problem correctly, but note that the branches in 'readMT' have identical implementations, the only difficulty is instantiating them at different hidden types, so that they try the appropriate 'Read' instances for those types. there's no need for different parsers beyond the 'Read' instances for every possible type. hiding concrete types in existentials sometimes only defers problems instead of solving them, but exposing class interfaces instead of types is a useful way to mitigate that effect. it just so happens that this particular problem, reading an existential type, slightly exceeds that pattern, as 'read' needs to know the hidden type to do its job ('read' does not determine the type from the input form, but uses the type to determine what form.the input should have). a workaround is to try to read all possible types, then hide the type again once a match is found. the main disadvantage of this method is that we need a list of all the types that could possibly be hidden in 'MyType' (or at least a list of all the types that we expect to find hidden in 'MyType' when we read it). we can, however, abstract out that list of types, and write a general type-level recursion to try reading every type in such a list: class ReadAsAnyOf ts ex -- read an existential as any of hidden types ts where readAsAnyOf :: ts -> ReadPrec ex instance ReadAsAnyOf () ex where readAsAnyOf ~() = mzero instance (Read t, Show t, MyClass t, ReadAsAnyOf ts MyType) => ReadAsAnyOf (t,ts) MyType where readAsAnyOf ~(t,ts) = r t `mplus` readAsAnyOf ts where r t = do { m <- readPrec; return (MT (m `asTypeOf` (t,0))) } -- a list of hidden types hidden = undefined :: (TipoA,(TipoB,())) readMT :: ReadPrec MyType readMT = prec 10 $ do Ident "MT" <- lexP parens $ readAsAnyOf hidden -- r T1a `mplus` r T1b
Thanks for your kind attention.
you're welcome!-) reading existentials (or gadts, for that matter) is an interesting problem. sometimes too interesting.. claus
On Mon, Jul 09, 2007 at 09:41:32PM +0100, Claus Reinke wrote:
i'm not sure i understand the problem correctly, but note that the branches in 'readMT' have identical implementations, the only difficulty is instantiating them at different hidden types, so that they try the appropriate 'Read' instances for those types. there's no need for different parsers beyond the 'Read' instances for every possible type.
This is now clear.
hiding concrete types in existentials sometimes only defers problems instead of solving them, but exposing class interfaces instead of types is a useful way to mitigate that effect. it just so happens that this particular problem, reading an existential type, slightly exceeds that pattern, as 'read' needs to know the hidden type to do its job ('read' does not determine the type from the input form, but uses the type to determine what form.the input should have).
That's exactly what I had in mind. But I ignored the specific problem of reading: "'read' uses the type", and the type is hidden..
a workaround is to try to read all possible types, then hide the type again once a match is found. the main disadvantage of this method is that we need a list of all the types that could possibly be hidden in 'MyType' (or at least a list of all the types that we expect to find hidden in 'MyType' when we read it).
we can, however, abstract out that list of types, and write a general type-level recursion to try reading every type in such a list:
class ReadAsAnyOf ts ex -- read an existential as any of hidden types ts where readAsAnyOf :: ts -> ReadPrec ex
[...]
-- a list of hidden types hidden = undefined :: (TipoA,(TipoB,()))
readMT :: ReadPrec MyType readMT = prec 10 $ do Ident "MT" <- lexP parens $ readAsAnyOf hidden -- r T1a `mplus` r T1b
This is a nice work around indeed and could be suitable for my specific problem. Thank you very much: this thread perfectly clarified the issue I was facing. Most kind of you. BTW, I have the feeling that existential types should be used with extreme care since they open up great possibilities of really hidden bugs: in other word, it seems to me they could be use to just trick the type checker. Sort of scary. Am I right? Thanks Andrea
reading existentials (or gadts, for that matter) is an interesting problem. sometimes too interesting..
http://www.padsproj.org/ is a project that allows automated reading codde for even some dependently-typed data. Perhaps it has something to offer for automatic deriving of Read instances for GADTs? Jim
On Mon, Jul 09, 2007 at 09:41:32PM +0100, Claus Reinke wrote:
hiding concrete types in existentials sometimes only defers problems instead of solving them, but exposing class interfaces instead of types is a useful way to mitigate that effect. it just so happens that this particular problem, reading an existential type, slightly exceeds that pattern, as 'read' needs to know the hidden type to do its job ('read' does not determine the type from the input form, but uses the type to determine what form.the input should have). a workaround is to try to read all possible types, then hide the type again once a match is found. the main disadvantage of this method is that we need a list of all the types that could possibly be hidden
As a follow up, mainly meant to thank you, I wanted to let you know that I adopted this approach in a piece of software I'm writing. It's a status bar for the XMonad Window Manager, the tiling WM written in Haskell.[1] Actually it is a text based status bar that can be used with any WM, but we love XMonad particularly...;-) More information about this status bar can be found here: http://www.haskell.org/pipermail/xmonad/2007-July/001442.html with link to the source code, a screen shot and eve a link to a binary. I obviously credited you for the help and the code![2] One again, thank you. All the best, Andrea [1] http://xmonad.org/ [2] http://gorgias.mine.nu/repos/xmobar/Runnable.hs
participants (3)
-
Andrea Rossato -
Claus Reinke -
Jim Apple