EG
Или в компайл-тайме, не суть важно.
Size: a a a
2020 February 12
AZ
К счастью определять их не нужно, т.к. они уже даны)
К слову он так и определен
absurd :: Void -> a
absurd a = case a of {}AZ
в расте для невер-типов я тоже такое видел
AZ
он имхо это боттом
AZ
или вопрос в том что функция не должна его _возвращать_
AZ
но по идее любая композиция такого вида тоже гео возвращает
AZ
неявно, но суть та же
λ
match Empty не может быт вызыван
Ну так Empty и построен быть не может
EG
Если
F<T, U> это U, то задача решается тривиально.EG
Возможно, остальные случаи можно как-то свести к этому.
λ
хз, имхо это не соответствует условию "не должно быть боттомов"
> имхо
AZ
> имхо
мне лень делать эту приписку ко всем утверждениям что я пишу
𝙰𝙸
К слову он так и определен
absurd :: Void -> a
absurd a = case a of {}Ох. Ну я говорил про входные аргументы quiz_1 и quiz_2. Там боттомов нет.
AZ
но иногда стоит подчеркнуть
λ
мне лень делать эту приписку ко всем утверждениям что я пишу
Тебя не смущает, что в языках, где запрещен боттом, матчится по лжи можно?
AZ
AZ
ну ок
AZ
уговорил
λ
Просто если было бы нельзя, то нельзя было бы написать функцию
getJust : (ma : Maybe a) -> {isJust ma = true} -> aλ
А так как можно, то в кейсе
Nothing выводят ложь и через абсурд получают "значение типа" a