[laureny]

> write your types and your programs write themselves as the "only possible implementation".

But there are only very few type signatures for which this is true, even if you stick to totality.

[tel]

In practice types often winnow the possible implementations to be a relatively small set. This effect is improved if you also include notions of law-abiding implementations as Haskellers often do. At the end of the day, it's true that implementations (don't yet) write themselves, but, more realistically, that the constraints of type and theory drive you naturally to the correct solutions even if you never once figure out the "operational" aspect.

That occurs quite often.

[ademarre]

> law-abiding implementations

Are you referring to category laws?

[dllthomas]

Lots of typeclasses have associated "laws" that well-behaved instances are expected to abide by.

[laureny]

But these are not enforceable by the type system (at least in Haskell), kind of supporting my point that types alone are rarely sufficient :)

[dllthomas]

I don't think anyone believes that types are sufficient outside, at least outside of a dependently typed language (at which point you'll have more diversity of opinion).

[tel]

Types in Haskell won't buy you 100% of what you need, but they may buy you 50%.