Числа церкви в F #

В приведенном ниже объяснении я буду использовать определение type CN<'a> = ('a -> 'a) -> 'a -> 'a (где «CN» означает «Церковное число»), чтобы сократить объяснение и уменьшить беспорядок.

Ваша попытка применить c2 к cPred не удалась, потому что c2 ожидает аргумент типа 'a -> 'a, а cPred не является такой функцией.

Вы можете ожидать, что cPred будет соответствовать ожидаемому типу, потому что вы объявили его как CN<'a> -> CN<'a>, но это не истинный тип. Поскольку вы применяете аргумент cn к типу bool*CN<'a> -> bool*CN<'a> (который является типом cSucc), компилятор делает вывод, что cn должен иметь тип CN<bool*CN<'a>>, и поэтому cPred получает тип CN<bool*CN<'a>> -> CN<'a>, что не соответствует тому, что ожидает c2.

Все это сводится к следующему факту: функции теряют свою универсальность, когда вы передаете их как значения.

Рассмотрим более простой пример:

let f (g: 'a -> 'a list) = g 1, g "a"

Такое определение не будет компилироваться, потому что 'a является параметром f, а не параметром g. Следовательно, для данного исполнения f должен быть выбран конкретный 'a, и это не может быть одновременно и int, и string, и, следовательно, g не может применяться одновременно к 1 и "a".

Точно так же cn в cPred закрепляется за типом bool*CN<'a> -> bool*CN<'a>, что делает тип самого cPred несовместимым с CN<_>.

В простых случаях есть очевидный обходной путь: дважды передать g.

let f g1 g2 = g1 1, g2 "a"
let g x = [x]
f g g
// > it : int list * string list = [1], ["a"]

Таким образом, g оба раза потеряет универсальность, но будет специализирован к разным типам - первый экземпляр к int -> int list, второй - к string -> string list.

Однако это лишь полумера, подходящая только для самых простых случаев. Общее решение потребует от компилятора понимания того, что мы хотим, чтобы 'a было параметром g, а не параметром f (это обычно называют "тип более высокого ранга"). В Haskell (точнее, в GHC) есть простой способ сделать это с расширением RankNTypes включено:

f (g :: forall a. a -> [a]) = (g 1, g "a")
g x = [x]
f g
==> ([1], ["a"])

Здесь я явно сообщаю компилятору, что параметр g имеет собственный универсальный параметр a, включив forall a в объявление его типа.

F# не имеет такой явной поддержки для этого, но предлагает другую функцию, которую можно использовать для достижения того же результата — интерфейсы. Интерфейсы могут иметь универсальные методы, и эти методы не теряют универсальности при передаче экземпляров интерфейса. Таким образом, мы можем переформулировать приведенный выше простой пример следующим образом:

type G = 
    abstract apply : 'a -> 'a list

let f (g: G) = g.apply 1, g.apply "a"
let g = { new G with override this.apply x = [x] }
f g
// it : int list * string list = ([1], ["a"])

Да, синтаксис для объявления таких «функций более высокого ранга» громоздкий, но это все, что может предложить F#.

Итак, применяя это к вашей исходной проблеме, нам нужно объявить CN в качестве интерфейса:

type CN = 
    abstract ap : ('a -> 'a) -> 'a -> 'a

Затем мы можем построить некоторые числа:

let c0 = { new CN with override __.ap f x = x }
let c1 = { new CN with override __.ap f x = f x }
let c2 = { new CN with override __.ap f x = f (f x) }
let c3 = { new CN with override __.ap f x = f (f (f x)) }
let c4 = { new CN with override __.ap f x = f (f (f (f x))) }

Затем cSucc и cPred:

let cSucc (b,(cn:CN)) = 
    if b 
    then (b, { new CN with override __.ap f x = f (cn.ap f x) }) 
    else (true, cn)

let cPred (cn:CN) = snd (cn.ap cSucc (false, c0))

Обратите внимание, что cPred теперь имеет предполагаемый тип CN -> CN, что нам и нужно.
Арифметические функции:

let cAdd (cn: CN) (cm: CN) = { new CN with override __.ap f x = cn.ap f (cm.ap f x) }
let cMult (cn: CN) (cm: CN) = { new CN with override __.ap f x = cn.ap cm.ap f x }
let cSub (cn: CN) (cm: CN) = cm.ap cPred cn

Обратите внимание, что все они получают предполагаемый тип CN -> CN -> CN, как и ожидалось.

И, наконец, ваши примеры:

let f = (fun x -> x + 1)

//This works
((cPred << cPred) c3).ap f 0

//This also works now
(c2.ap cPred c3).ap f 0