[Haskell] Implicit Parameters

[Robert Dockins]

On Feb 27, 2006, at 3:31 PM, Ashley Yakeley wrote:

> Ben Rudiak-Gould wrote:
>> I'd advise against using implicit parameters, because (as you've  
>> seen) it's hard to reason about when they'll get passed to functions.
>
> And Johannes Waldmann wrote:
> > Implicit parameters are *evil*. They seem to simplify programs
> > but they make reasoning about them much harder.
>
> Feh. Implicit parameters are often exactly what you want. You just  
> have to make sure to provide type signatures (-Wall -Werror can  
> help here).
>
> In fact it would be useful to allow implicit parameters and other  
> type context at the top level of a module:
>
>   forall m. (Monad m,?getCPUTime :: m Integer) => module MyModule  
> where
>     timeFunction :: forall a. m a -> m (Integer,a)
>     timeFunction ma = do
>       t0 <- ?getCPUTime
>       a <- ma
>       t1 <- ?getCPUTime
>       return (t1 - t0,a)
>
> This is just syntactic sugar that gives this:
>
>   timeFunction :: forall m a. (Monad m,?getCPUTime :: m Integer) =>
>      m a -> m (Integer,a)
>
> In a future Haskell Operating System, this is how system functions  
> could be provided to application code. This would make secure  
> sandboxes easy to set up, for instance.

That's pretty similar in spirit to the "Sections" mechanism available  
in Coq.  (http://coq.inria.fr/doc/Reference-Manual004.html#toc13)

Basically, it lets you declare a lexical region where all definitions  
can assume certain variables are in scope with particular types.   
Outside the section, the definitions are "generalized", so that the  
definitions in the section are extended with additional lambdas.  I  
can make complicated type signatures a lot shorter, easier to  
understand and more robust against changes.

Has something like this ever been discussed as a possible Haskell  
language feature?


Rob Dockins

Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
           -- TMBG