[tel]

Well, as you go to the next steps you can use proof search techniques to do exactly that: write your types and your programs write themselves as the "only possible implementation".

This is already possible sometimes in Haskell so long as we restrict ourselves from pathological values like exceptions and non-termination. In fact, the first place this phrase shows up is Russel O'Connor talking about highly polymorphic lens code.

http://r6.ca/blog/20120708T122219Z.html

This kind of type limitation of possible implementations is called parametricity and is difficult to encounter even in most typed languages as it requires purity.

[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%.

[dllthomas]

The first place which phrase shows up?

[tel]

Mm, I think I went too far there. I was thinking "confession of a Haskell hacker" but got that conflated with "if it types, it's right".