[Haskell-cafe] Re: If wishes were horses...

[wren ng thornton]

Ben Millwood wrote:
> In general, laziness behaviour can
> get complicated quickly and so I'm not convinced that the type
> signature is a good home for that information.

Certainly it can. A lot of the same problems arise in the logic 
programming community under the topic of "modes", i.e. whether a logic 
variable must be ground (or rather, how defined it must be) before it's 
safe to "run the function backwards". Though, at present AFAIK, they've 
contented themselves with rough approximations like lifted/unlifted 
value types or strict/lazy arrows, either of which can catch the simple 
cases.

Personally, I think the only way to capture *all* strictness information 
is if we have full dependent types (or worse, for logic languages, since 
their dependencies lack the directionality of usual dependent types). If 
we had full dependent types, and went with the lifted/unlifted 
distinction instead of the strict/lazy one, then we could give `maybe` 
the type:

     maybe :: (_:b) -> (_:a -> b') -> (m:Maybe a)
              -> (case m of Nothing => b ; Just _ => b')

Would such a type be helpful? <shrug>  I think adding full dependent 
types is a bit much if all we're interested in is strictness behavior. 
But, as you say, it seems very unlikely that we can encode strictness 
behaviors which may depend on particular runtime values without DTs.

-- 
Live well,
~wren