LINUX.ORG.RU

Непонятки с частичным применением

 


0

1
num 0 _ b = b
num n f b = f $ num (n-1) f b

exp' m n f b = (num n (num m)) f b

Есть функция возведения в степень на нумералах Черча, работает так:

exp' 2 10 (+1) 0

Будьте добры, подскажите, почему и как работает вот это:

num n (num m)

Спасибо!


Без частичного применения видимо было бы так:

num 0 _ b x = b
num n f b x = f $ num (n-1) f b

exp' m n f b = (lambda f b: num n (lambda x y z: num m x y z) f b) f b = num n (lambda x y z: num m x y z) f b

monk ★★★★★
()

Число n — это комбинатор, который из некоторой функции f делает n'ую степень этой функции. То есть, например: zero f = id; one f = f; two f = f . f; three f = f . f . f; и т.д. Поэтому когда есть нумерал m и надо найти m ^ n, то надо лишь применить n к m.

nezamudich ★★
()

советую для начала выписать типы, будет проще, честно говорю.

qnikst ★★★★★
()
Ответ на: комментарий от nezamudich

Спасибо. И все же непонятно, как нумерал с типом:
num n :: (t -> t) -> t -> t
применяется к другому нумералу с тем же типом и в итоге получаем тот же самый тип.

При этом одинаковый тип у
(num n (num m))
и
num n . num m
но результат их применения к (+1) 0 разный.

tuxin
() автор топика
Ответ на: комментарий от tuxin

применяется к другому нумералу с тем же типом и в итоге получаем тот же самый тип.

Полиморфизм же. (num n) :: (a -> a) -> (a -> a), (num m) :: (b -> b) -> (b -> b). Чтобы применить (num n) (num m), надо унифицировать их типы. В данном случае a = b -> b. Получаем (num n) :: ((b -> b) -> (b -> b)) -> ((b -> b) -> (b -> b)), который уже можно смело применять к (num m) :: (b -> b) -> (b -> b).

но результат их применения к (+1) 0 разный.

Нет же. Одинаковый.

Prelude> (num 10) (num 2) (+ 1) 0
1024
Prelude> exp' 2 10 (+ 1) 0
1024
nezamudich ★★
()
Ответ на: комментарий от tuxin

А, ну первое — это произведение же. (num n) . (num m) $ f = num n (num m f). Это совсем не num n (num m) f, тут другой порядок применения.

nezamudich ★★
()
Ответ на: комментарий от nezamudich

Возьмем умножение:
mult m n f b = num m (num n f) b

По определению num я могу представить как это работает:
mult 3 2 (+1) 0 = num 3 (num 2 (+1)) 0 =
= num 2 (+1) $ num 2 (+1) $ num 2 (+1) $ 0 =
= (+1) $ (+1) $ (+1) $ (+1) $ (+1) $ (+1) $ 0

С возведением в степень никак не получается. Помоги, пожалуйста.

tuxin
() автор топика
Ответ на: комментарий от tuxin
pow 3 2 (+ 1) 0 = num 2 (num 3) (+ 1) 0 = (num 3 . num 3) (+ 1) 0 = (num 3) ((num 3) (+ 1)) 0 = ((num 3) (+ 1)) . ((num 3) (+ 1)) . ((num 3) (+ 1)) $ 0 = ((+ 1) . (+ 1) . (+ 1)) . ((+ 1) . (+ 1) . (+ 1)) . ((+ 1) . (+ 1) . (+ 1)) $ 0 = 9 
nezamudich ★★
()
Ответ на: комментарий от tuxin

Сорри, конечно же так правильно:

num 0 _ b = b
num n f b = f $ num (n-1) f b

tuxin
() автор топика
Ответ на: комментарий от tuxin

По определению num: num 2 f = f . f; ну либо эквивалентно num 2 f x = f (f x).

nezamudich ★★
()
Ответ на: комментарий от tuxin

Нумералы Чёрча — это же не про хаскель, это про лямбда-исчисление. Оно одинаково относится ко всем языкам из семейства ML. Собственно, про это и читать можно где угодно.

А что ботать про сам хаскель лучше меня расскажет qnikst, а то я начну всякое старьё рекомендовать типа Плазмейера, может оно уже и не актуально.

nezamudich ★★
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.