Наш профессор попросил нас подумать о функции в OCaml, которая имеет тип
'a -> 'b
т.е. функция одного аргумента, которая может быть чем угодно, и которая может возвращать что угодно другое.
Я думал об использовании raise
в функции, которая игнорирует ее аргумент:
let f x = raise Exit
Но профессор сказал, что есть решение, которое не требует каких-либо функций в стандартной библиотеке. Я в замешательстве: как вы можете сделать это, 'b
если у вас его нет вообще?
Я спрашиваю здесь, а не о переполнении стека, потому что я хочу понять, что происходит, я не хочу просто видеть программу без объяснения причин.
programming-languages
typing
functional-programming
Жиль "ТАК - перестань быть злым"
источник
источник
raise
будет работать, поэтому мы знаем, как лучше всего объяснить, почему работает решение, которое ищет ваш профессор (которое будет работать по тем же причинам, что иraise
работает).raise : exn -> 'a
чтобы я мог получить возвращаемое значение, я просто игнорирую аргумент.Ответы:
Скелет есть
let f x = BODY
. В BODY вы должны использовать x только общими способами (например, не отправлять его функции, ожидающей целые числа), и вы должны возвращать значение любого другого типа. Но как последняя часть может быть правдой? Единственный способ удовлетворить утверждение «для всех типов'b
, возвращаемое значение - это значение типа'b
» - это убедиться, что функция не возвращает. Существует ровно две возможности: либо неисправность ТЕЛА, либо она не прекращается. Функция не работаетraise
, следующее не завершается:источник
Сначала несколько замечаний. Использование только лямбда-исчисления с типизированным ядром невозможно получить,
'a -> 'b
потому что система типизации соответствует (через изоморфизм Карри Ховарда ) интуиционистской логике, и соответствующая формулаA → B
не является тавтологией.Другие расширения, такие как кортежи и сопоставления / условия, все еще сохраняют некоторую логическую согласованность, добавляя типы продуктов,
*
которые соответствуют логическим связям, и , и типы сумм,|
которые соответствуют или . Опять же, не ожидайте, что они произведут этот'a -> 'b
тип, поскольку это позволит доказать некоторую формулу, которая не является тавтологией.Таким образом, ваши единственные возможности - использовать другие конструкции, которые выходят из логики, например
raise
(но в этом случае вы не можете)… илиlet rec
! Рекурсия позволяет создавать программы, которые никогда не завершаются, и их результатам может быть присвоен произвольный тип возврата, поскольку они никогда не будут созданы. Теперь, если вы думаете о самой тривиальной не завершающей функции (той, которая непосредственно вызывает себя, чтобы вернуть результат):Вы заметите, что его тип точно
'a -> 'b
: какой бы ни был предоставленный аргумент, можно предположить, что результат (который никогда не будет вычислен) имеет любой тип.Конечно, это
f
не интересная функция, но в этом суть. В OCaml любая функция, тип которой не похож на правильную формулу, является подозрительной функцией.источник
Используя примитив компилятора, вы можете написать это:
(и действительно, дистрибутив компилятора обеспечивает это, хотя и не является частью языка). Это небезопасный актерский состав.
Ваш профессор почти наверняка не хочет этого. Однако это также единственная полезная функция с типом,
'a -> 'b
о которой я знаю, и она действительно используется в самом дистрибутиве OCaml.источник