17 Mar
2011
17 Mar
'11
4 p.m.
On 2011-03-17 19:35, wren ng thornton wrote:
Dependently typed languages tend to use the second definition because it gives a pure total function (unlike the first) and because it's less obnoxious to use than the third. In Haskell the third would be even more obnoxious.
There is a fourth option: a comparison view. See "The view from the left" by Conor McBride and James McKinna (Section 6). (This option is similar to what Henning Thielemann suggested.) -- /NAD