[Haskell-cafe] Strict type system allows for a maximum number of programming errors to be caught at compile time.

[Casey McCann]

On Tue, May 4, 2010 at 12:13 AM, Ivan Miljenovic
<ivan.miljenovic at gmail.com> wrote:
> On 4 May 2010 13:30, Luke Palmer <lrpalmer at gmail.com> wrote:
>> Here is a contrived example of what I am referring to:
>>
>> prefac f 0 = 1
>> prefac f n = n * f (n-1)
>>
>> fac = (\x -> x x) (\x -> prefac (x x))
>
> I can't work out how this works (or should work rather); is it meant
> to be using church numerals or something (assuming that they have been
> made an instance of Num so that - and * work)?

Looks like a variation on H. Curry's fixed-point combinator to me, e.g.:

y f = (\x -> f (x x)) (\x -> f (x x))

Which of course is perfectly useful, but not valid in any type system
that excludes absurdities. The otherwise-infinite type signature for Y
is circumvented by built-in recursion in Haskell (making halting
undecidable in the process, unfortunately).

- C.