𝙰𝙸
/me неочевидно, чем это решение более тотальное, чем
Он возвращает
loop { }.Он возвращает
!Вот Empty - да. Empty - это !, а match a {} - это Т)
Size: a a a
2020 February 12
EG
[citation needed]
EG
#![feature(never_type)]
fn f<T>(x: !) -> T {
x
}
Компилируется.
match Empty {} имеет тип ! и коэрсится после этого в любой тип T.λ
#![feature(never_type)]
fn f<T>(x: !) -> T {
x
}
Компилируется.
match Empty {} имеет тип ! и коэрсится после этого в любой тип T.нет
EG
нет
[citation needed]
λ
match a {} имеет тип тела матчинга, а так как тела нет, то и тип доступен любой, какой пожелаешь
λ
это один из фундаментальных законов как классической логики, так и интуиционистской
λ
из лжи выводимо всё что угодно
λ
коэрция
! в любой тип сделана лишь для удобства, чтобы не нужно было писать:let a = loop {};
match a {}𝙰𝙸
#![feature(never_type)]
fn f<T>(x: !) -> T {
x
}
Компилируется.
match Empty {} имеет тип ! и коэрсится после этого в любой тип T.Вообще да, !, как и Empty - это путая дизъюнкция, но, строго говоря, сама по себе она выводом не является. Чтобы сделать вывод из дизъюнкции вам нужно иметь соответствующую лемму для каждого дизъюнкта. В нашем случае дизъюнктов 0, поэтому и лемм 0. Пустой матч - цивилизованный способ это сказать.
AZ
Вообще да, !, как и Empty - это путая дизъюнкция, но, строго говоря, сама по себе она выводом не является. Чтобы сделать вывод из дизъюнкции вам нужно иметь соответствующую лемму для каждого дизъюнкта. В нашем случае дизъюнктов 0, поэтому и лемм 0. Пустой матч - цивилизованный способ это сказать.
хз, имхо это не соответствует условию "не должно быть боттомов"
AZ
match Empty не может быт вызыван
EG
В третьей задаче боттом у нас вообще на входе.
AZ
по сути Empty никогда не возвращает результат
AZ
В общем если сформулировать "написать без циклов, рекурсии и паники" то такой вариант можно принять
EG
На самом деле, у нас в каждой задаче на входе боттом, потому что функции
l, r и a нельзя определить без боттомов.AZ
в общем, не очень понятно, что такие задачки должны показать
𝙰𝙸
На самом деле, у нас в каждой задаче на входе боттом, потому что функции
l, r и a нельзя определить без боттомов.К счастью определять их не нужно, т.к. они уже даны)
EG
Забавно, в первых двух задачах типы на входе автоматически имплементируют
Any, что позволяет сделать некоего рода небесконечную рекурсию.EG
Это значит, что мы умеем сравнивать типы этих значений в рантайме.