[Haskell-cafe] hint and type synonyms

[Daniel Gorín]

Hi

I think I see now what the problem you observe is. It is not related with type synonyms but with module scoping. Let me briefly discuss what hint is doing behind the scenes and why, this may give a better understanding of what kind of things will and will not work.

While hint is directly tied to ghc, it should be possible to implement something similar for any self-hosting Haskell compiler. Essentially, you need the compiler to provide a function compileExpr that given a string with a Haskell expression, returns a value of some type, say CompiledExpr (or an error if the string is not a valid expression, etc). So, for instance, 'compileExpr "not True"' will produce something of type CompiledExpr, but we know that it is safe to unsafeCoerce this value into one of type Bool.

Now, what happens if one unsafeCoerces to a Bool the result of running compileExpr on "[True]"? This is, of course, equivalent to running '(unsafeCoerce [True]) :: Bool' and sounds dangerous. Indeed, if your compiler were to keep type information in its CompiledExprs and check for type correctness on each operation (akin to what the interpreters for dynamic languages (like Perl, Ruby, etc.) do) then you may get a gracious runtime error; but most (if not all) of Haskell compilers eliminate all type information from the compiled representation (which is a good thing for performance), so the result of a bad cast like the one above will surely result in an ugly (uninformative) crash.

So how does we deal with this in hint? When you write 'interpret "not True" (as :: Bool)' we want a runtime guarantee that "not True" is in fact a value of type Bool. We do this by calling compileExpr with "(not True) :: Bool" instead of just with "not True". This way, an incorrect cast is caught at runtime by compileExpr (e.g. "([True]) :: Bool" will fail to compile). In order to do this, the type parameter must be an instance of Data.Typeable and we use the typeOf function to obtain the type (e.g. show $ Data.Typeable.typeOf "True" == "Bool")

This is, as you've noticed, a little fragile. For this to work, the type expression returned by Data.Typeable.typeOf must correspond to something that is visible to the complieExpr function. You do this in hint adding the relevant modules with the setImports function. It may be a little inconvenient, but I think it is unavoidable.

I wouldn't ever recommend writing bogus instances of Typeable as in your original example. If you find a situation where this looks as the more sensible thing to do I'd like to know! Also, in the example from Rc43 you cite below, instead of running setImport on HReal.Core.Prelude you need to run setImport on all the modules that are exported by HReal.Core.Prelude (this can be abstracted in a function, I guess).

Since I am on this, I'd like to point out that this solution is, sadly, not 100% safe. There is still one way in which things can go wrong and people often trip over this. The problem roughly comes when your program defines a type T on module M and ends up running compileExpr on an expression of type M.T but in a way such that module M gets to be compiled from scratch. When this happens, the type M.T on your program and the type M.T used in compileExpr may end up having two incompatible representations and the unsafeCoerce will lead to a crash. This typically happens when using hint to implement some form of plugin system. Imagine you have a project organized as follows:

project/
project/src/M.hs
project/src/main.hs
project/plugins/P.hs
dist/build/M.o
dist/build/main.o
dist/build/main

where M.hs defines T;  P.hs imports M and exports a function f :: T; and main.hs imports M and runs an interpreter that sets "src" as the searchPat, loads "plugins/P.hs", interprets "f" as a T and does something with it. Assume dist/build/main is run from the project dir. When hint tries to load "plugins/P.hs" the "import M" will force the compiler to search for module M.hs in project/src and compile it again (just like ghci would do). This can be bad! The robust solution in this case is to put all the definitions that you want to be shared by your program and your dynamically loaded code in a library (and make sure that it is installed before running the program).

Hope this helps...

Daniel




On Mar 31, 2012, at 8:06 PM, Claude Heiland-Allen wrote:

> Hi Daniel, cafe,
> 
> On 31/03/12 17:47, Daniel Gorín wrote:
>> Could you provide a short example of the code you'd like to write but gives you problems? I'm not able to infer it from your workaround alone...
> 
> This problem originally came up on #haskell, where Rc43 had a problem making a library with a common module that re-exports several other modules:
> 
> http://hpaste.org/66281
> 
> My personal interest is somewhat secondary, having not yet used hint in a real project, but code I would like to write at some point in the future is much like the 'failure' below, unrolled it looks like:
> 
> main = (print =<<) . runInterpreter $ do
>  setImports ["Prelude"]
>  interpret "1/5" (as :: Rational)
> -- fails
> 
> Having to remember that Rational is defined as type Rational = Ratio Integer and that Ratio is defined in Data.Ratio and then to add that to the setImports list is a little inconvenient:
> 
> main = (print =<<) . runInterpreter $ do
>  setImports ["Prelude", "Data.Ratio" ]
>  interpret "1/5" (as :: Rational)
> -- works
> 
> But for my own purposes this is probably much saner in the long run than my newtype wrapping approach below.
> 
> However, this is not always possible: supposing Ratio itself was defined as a type synonym of Ratio2, and Ratio2 was not exported.  Perhaps this is what Rc43 was experiencing, but I shouldn't speculate, as this is all getting a bit theoretical - I should try out hint in the real world to see if this problem makes things impractical for me - sorry for the noise!
> 
> Thanks,
> 
> 
> Claude
> 
>> Thanks,
>> Daniel
>> 
>> 
>> On Mar 31, 2012, at 6:19 PM, Claude Heiland-Allen wrote:
>> 
>>> Hi all,
>>> 
>>> What's the recommended way to get hint[0] to play nice with type synonyms[1]?
>>> 
>>> A problem occurs with in scope type synonyms involving types not in scope.
>>> 
>>> I came up with this after looking at the source[2], but it makes me feel ill:
>>> 
>>> --8<--
>>> -- hint and type synonyms don't play nice
>>> module Main where
>>> 
>>> import Language.Haskell.Interpreter
>>> 
>>> import Data.Typeable as T
>>> import Data.Typeable.Internal
>>> import GHC.Fingerprint.Type
>>> 
>>> main = failure>>  success
>>> 
>>> test t = (print =<<) . runInterpreter $ do
>>>  setImports [ "Prelude" ]
>>>  interpret "1/5" t
>>> 
>>> failure = test (as :: Rational)
>>> -- Left (WontCompile [GhcError {errMsg = "Not in scope: type constructor or class `Ratio'"}])
>>> 
>>> success = test (as :: Q)
>>> -- Right (1 % 5)
>>> 
>>> newtype Q = Q Rational
>>> 
>>> instance Show Q where
>>>  show (Q a) = show a
>>>  showsPrec n (Q a) = showsPrec n a
>>> 
>>> instance Typeable Q where
>>>  typeOf _ = TypeRep (Fingerprint 0 0) (T.mkTyCon "Rational") []
>>> --8<--
>>> 
>>> Thanks,
>>> 
>>> 
>>> Claude
>>> 
>>> [0] http://hackage.haskell.org/package/hint
>>> [1] http://www.haskell.org/onlinereport/decls.html#type-synonym-decls
>>> [2] http://hackage.haskell.org/packages/archive/hint/0.3.3.4/doc/html/src/Hint-Eval.html#interpret
>>> 
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>> 
> 
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe