[Haskell-cafe] Displaying infered type signature of 'offside' functions

[Jules Bean]

Simon Peyton-Jones wrote:
> | I like the strong static type system of Haskell for various
> | reasons. One reason is, that it makes easier to understand new
> | code. I.e. when I read code I type ':t foo' in ghci/hugs from
> | time to time, to check my own idea of the type signature, if it
> | is not included in the source code.
>
> The principal difficulties here are to do with "what do we want" rather the implementation challenges.
>
> 1.  Should the compiler print the type of every declaration? Should GHCi allow you to ask the type of a local decl?
>   

IMO, ghci should definitely allow you to ask. This comes up for me every 
time that I write any haskell code (and in general I end up hoisting 
local definitions to the top level, which is a real pain if there is 
local scope, data or type, to hoist with it).

> 2.  How should the variables be identified?  There may be many local bindings for 'f', so you can't say just ":t f".  Ditto if dumping all local bindings.
>
>   

I think this is a hard question. I was imagining some kind of 
hierarchical system like foo.f, in the case that f is locally defined 
inside foo. (Yes I know we can't easily use '.' for that). There might 
be might be multiple fs inside the definition of foo; indeed there might 
even be multiple fs nested inside each other.

I suspect the happy medium, rather than a formal way of accessing every 
possible position, is a contextually intelligent system which allows the 
user to disambiguate. So 'foo.f' will show all the fs inside foo if 
there are, say, fewer than 5, or otherwise ask for more guidance.

> 3.  Do you want all locally-bound variables (including those bound by lambda or case), or just letrec/where bound ones?   I think 'all', myself, but there are a lot of them.
>
>   

All, I think. (It's very common in multiple cases for the same name to 
be used repeatedly at the same type; this could be conveniently 
indicated concisely, perhaps).


> 4.  (This is the trickiest one.)  The type of a function may mention type variables bound further out.  Consider
>         f :: [a] -> Int
>         f xs = let v = head xs in ...
>
> The type of 'v' is simply 'a'.  Not 'forall a. a', but rather 'if xs:[a] then *that* a!'  In general there may also be existential type variables bound by an enclosing pattern match too.
>   

I think you're going to have to give the type context, in such cases.

(a :: *) |- v : a

... possibly with some way to access information about where the binding 
site for 'a' is.


> These are all user-interface issues.  If some people would like to thrash out a design, and put it on the Wiki, I think there is a good chance that someone (possibly even me) would implement it

That would be a good idea; my comments above do not a design make 
though. Can anyone else elaborate further?

Jules