On July 24, 2014 at 23:49:10, Simon Peyton Jones ([email protected]) wrote:
> | I think part of the confusion is coming from the fact that we don’t
> | process each module individually, resolve all of the types, and
> | serialize them to disk somewhere. Rather, when we check a module, we
> | parse in ALL of the specifications it could possibly refer to (using
> | the transitive closure of the module imports) and try to resolve all of
> | them before moving to the actual constraint generation and solving
> | step.
>
> Yes that makes more sense.
>
> But it's not a good fit with GHC's way of working. You want to take some
> random module M,
> parse it afresh to find its LIQUID bits, and then resolve what those things
> mean. But that
> *necessarily* means that you must reconstruct the top-level lexical
> environment,
> which is formed from the import and top-level declarations. Constructing this
> environment
> -- the GlobalRdrEnv -- is not a simple matter. Much of RnNames does precisely
> that.
>
> Alas, we do not serialise this environment into M's interface file M.hi. We
> could do so,
> and doing so would be somewhat useful for GHCi, but it's absolutely not
> needed in the usual
> way of things.
This is basically what I expected, and I wouldn’t want to argue for adding more
things to the .hi files unless there are other compelling use cases.
> So I suppose what you could do is to reconstruct it afresh using GHC's
> existing code to
> do so. If you call RnNames.rnImports on the import declarations of your
> module, you'll
> get back a GlobalRdrEnv in which you can look up the RdrNames that occur in
> the LIQUID declarations.
>
> Actually that'll deal only with the imported things. You also want the
> locally defined
> top-level things. To do that you could use things like getLocalNonValBinders
> (see the
> call in RnSource.rnSrcDecls), but it might be easier to take the TypeEnv
> computed from
> the module's interface file, and turn that back into a bunch of global
> binders.
>
> But it's not so easy. What about
>
> module M( f ) where
>
> {-# LIQUID f :: { x | ...g... } -> Int
> f = blah
>
> g = blah
>
> Here g is only mentioned form f's LIQUID spec. So g will have disappeared
> altogether from
> M's interface file, discarded as dead code.
Thanks for these pointers! I’m not too concerned about the dead code issue
since Liquid Types generally won’t refer to top-level binders (they’re either
going to be functions, which can’t appear in the types in the first place, or
constants, which can be inlined).
> The natural alternative would be to serialise the LIQUID things into M.hi.
> That would
> entail parsing and renaming them in GHC, and extending the interface file
> format to handle
> it. I think it would be simpler. But it would be a bit more invasive of GHC.
>
>
> There is some support for serialising random stuff into interface files,
> called "annotations".
> You write
> {-# ANN f #-}
> and GHC will record in the interface file that f is associated with
> expression. See
> http://www.haskell.org/ghc/docs/latest/html/users_guide/extending-ghc.html#annotation-pragmas
>
Yes, I’ve looked at the annotations stuff in the past and have imagined
converting LiquidHaskell to a GHC Plugin that pulls the types out of
annotations. I *think* it could work, though there are two immediate wrinkles:
1. The docs say that annotations can only be applied to top-level
binders/declarations. We’ve found it *very* helpful to annotate nested binders
in some cases to reduce the inference burden (it’s also extremely helpful for
debugging the code/spec). Is this restriction in place because of the
aforementioned issue of not serializing the GlobalRdrEnv? If so, could the
restriction be lifted with the caveat that annotations on nested binders will
*not* be exported? I think that would be sufficient for us as long as we can
get a hold of the Core before any sort of inlining happens.
2. The docs say that you can only annotate binders that are declared in the
same module. We’ve similarly found it useful to be able to *assume* stronger
types for certain imported functions, though this is of course unsound. Could
we also lift the same-module restriction, again with the caveat that the
annotations will *not* be exported?
These are just some things to think about, I doubt I would have time to attempt
serious changes to LiquidHaskell along these lines until next year at the
earliest.
> Maybe there's a neater way to do this, that neither involves changing GHC nor
> all the faff
> above. If so I'd be happy to change GHC to accommodate the neater way. I'd
> like GHC to accommodate
> extensions like LH much more easily.
I still think that a Template Haskell-based approach could be really nice
without requiring any changes to GHC (beyond the profiling issue we’ve run
into). The reason I like this idea is that it feels more lightweight to me,
users would just express their specifications as Haskell values, and they (and
we) wouldn’t have to worry about making sure that the right flags are passed to
GHC to find imported modules etc.
Has anyone ever tried to blend Template Haskell with Annotations/Plugins? I’m
imagining something like the following
t_head = head ::: [liquid| {v:[a] | length v > 0} -> a|]
head [] = error
head (x:xs) = x
{-# ANN head t_head #-}
Here the spec for head exists alongside the implementation as a Haskell value,
so it’s immediately available for other tools to build on top of, but it’s also
attached to head as an Annotation so that Plugins like a future version of the
liquidhaskell verifier, or perhaps an optimization pass, can make use of it
during compilation. The ANN pragma seems a bit redundant here, but I really
like the idea of having these types readily available at multiple levels and I
don’t quite see how to accomplish that with Template Haskell or Annotations
alone.
Thanks for all of the comments!
Eric
_______________________________________________
ghc-devs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/ghc-devs
