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