Re: [Haskell-cafe] Displaying infered type signature of 'offside' functions
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Displaying infered type signature of 'offside' functions
Jules Bean [EMAIL PROTECTED] wrote,
concerning the problem of getting at the types of local definitions:
Simon Peyton-Jones wrote:
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 just wanted to contribute a PRACTICAL TRICK I use:
* If the local definition is a pattern binding
f = ...
then I just add
f :: Ordering
* If the local definition is a, say binary, function binding
f p1 p2 = ...
then I just add
f :: Float - Double - Ordering
(Type does not matter for the number of function arrows you need to put;
only the syntactic arity of the bindings matters here.)
This relies on the fact that the types Float, Double, and Ordering
very rarely occur in my code --- pick your own.
Now the compiler gives you wonderful error messages
``cannot match type `x y z' against Ordering'' ---
so you replace ``Ordering'' with ``x y z''.
If there are type variables in ``x y z''
that come from the context,
take care that you have
{-# LANGUAGE ScopedTypeVariables #-}
at the beginning of your module
(after the {-# OPTIONS ...#-} line,
which should, as a matter of style,
NOT contain -fglasgow-exts
)
and the necessary ``forall ty1 ty2 ...'' in front of your the type
in the type signature of the enclosing definition.
At the cost of a re-compilation, this works wonderfully for me,
and is much less painful than hoisting AND exporting local definitions.
But even I still have some wishes open:
* It would be nice if this worked inside the do-notation, too:
do x :: Ordering
x - m
(This is curently a syntax error.)
* It would be nice if {-# LANGUAGE ScopedTypeVariables #-}
brought in no other extensions,
and if GHC would recommend
the appropriate LANGUAGE pragmas instead of -fglasgow-exts
when it determines that the user might have wanted some extension.
(What is the right Language.Extension for GADTs?)
Wolfram
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Displaying infered type signature of 'offside' functions
On 2 May 2007 16:16:57 -, [EMAIL PROTECTED] [EMAIL PROTECTED] wrote: * It would be nice if this worked inside the do-notation, too: do x :: Ordering x - m (This is curently a syntax error.) I think the following works with -fglasgow-exts: do (x :: Ordering) - m -- -David House, [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Displaying infered type signature of 'offside' functions
* It would be nice if this worked inside the do-notation, too: do x :: Ordering x - m (This is curently a syntax error.) I think the following works with -fglasgow-exts: do (x :: Ordering) - m I know, but it is not as nice! ;-) Wolfram ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Displaying infered type signature of 'offside' functions
[EMAIL PROTECTED] wrote: Jules Bean [EMAIL PROTECTED] wrote, concerning the problem of getting at the types of local definitions: Simon Peyton-Jones wrote: 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 just wanted to contribute a PRACTICAL TRICK I use: * If the local definition is a pattern binding f = ... then I just add f :: Ordering * If the local definition is a, say binary, function binding f p1 p2 = ... then I just add f :: Float - Double - Ordering (Type does not matter for the number of function arrows you need to put; only the syntactic arity of the bindings matters here.) This relies on the fact that the types Float, Double, and Ordering very rarely occur in my code --- pick your own. Why not just declare a type you don't use? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Displaying infered type signature of 'offside' functions
On Wed, May 02, 2007 at 04:16:57PM -, [EMAIL PROTECTED] wrote: Now the compiler gives you wonderful error messages ``cannot match type `x y z' against Ordering'' --- so you replace ``Ordering'' with ``x y z''. You could just use a rigid type variable: foo :: a foo = ... (What is the right Language.Extension for GADTs?) There is none. Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Displaying infered type signature of 'offside' functions
| 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? 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. 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. 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. So it's not easy to see how to report v's type. In general there is no type signature for f, which only makes matters worse, since there is no name to use for the in-scope type variable. 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. Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Displaying infered type signature of 'offside' functions
On 28/04/07, Georg Sauthoff [EMAIL PROTECTED] wrote: Well, I mention this, because I would like to integrate some lookup feature (for type signatures) into vim (if it doesn't exist yet). It's worth pointing out that Emacs's haskell-mode already has this. For anyone that uses the major mode but hasn't heard of the inf-haskell features: C-c C-t inferior-haskell-type: looks up a type of the function under point, built-in or user-defined. C-c C-i inferior-haskell-info: looks up the info, à la GHCi :info, of the identifer under point, built-in or user-defined. C-c M-. inferor-haskell-find-definition: jumps to the definition of the function, class or datatype etc. under point. See the Haskell wiki page [1] for more information. [1]: http://haskell.org/haskellwiki/Haskell_mode_for_Emacs#inf-haskell.el:_the_best_thing_since_the_breadknife -- -David House, [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Displaying infered type signature of 'offside' functions
On 29/04/07, David House [EMAIL PROTECTED] wrote: It's worth pointing out that Emacs's haskell-mode already has this. For anyone that uses the major mode but hasn't heard of the inf-haskell features: I did forget to mention that this won't help with your 'offside' functions, though. -- -David House, [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
