K
Есть два варианта, в одном из них рекурсивное вхождение заменяется на тип результата - и вот это Чёрч
Size: a a a
Типы в языках программирования, моделирования, представления знаний и жизни
505 membersпожаловаться на группу
2021 November 13
АП
просто думая что может быть как угодно, я могу называть типом то, что типом не является или не соответствует теории типов или ещё чему то.
[
Попробуй прочитать Пирса
KV
Boehm-Berarduccu если точнее
KV
Чёрч это в бестиповом, но то же самое
[
Класс, то что я и хотел услышать
AC
Хотите соответствовать теории типов -- используйте известную логическую систему. Не ошибётесь.
[
В общем, Черч это
true :: a -> a -> a
false :: a -> a -> a
true :: a -> a -> a
false :: a -> a -> a
[
Кстати, а как числа так энкодят?
K
data N
= O
| S N
elimN :: c -> (c -> c) -> c
```
a
N = a -> (a -> a) -> a
zero z s = z
succ z s = s (z s)
K
t-то у тебя откуда?K
Окей, а теперь верни в succ
K
succ :: N -> N
succ t z s = s t
[
Ты как s к z апплаишь?