V
т.к. ⊥ будучи типом с 0 инхабитантов является вроде как субтипом всех возможных типов
⊥ это же значение, а не тип
Size: a a a
2019 November 21
t
это не "пустой тип"? как я понял, это не значение, потому что значений этого типа как раз нет
V
теперь понял. значит, если бы Hask был категорией (которой он не является, но почему, я узнаю позже) - то было бы 3*3 функций, из них реализуемы только те, которые не от ⊥, так?
откуда берется 3*3? говорю же, что не 9
t
т.е. как я понял, нельзя получить терм типа ⊥
V
т.е. как я понял, нельзя получить терм типа ⊥
ок, если ⊥ обозначать пустой тип, то при чем тут он? мы же вроде Bool обсуждали и функции на нем
t
откуда берется 3*3? говорю же, что не 9
почему? если считать, что в Boolean включен боттом, то это
True -> ⊥
True -> True
True -> False
False -> ⊥
False -> True
False -> False
⊥ -> ⊥ (не реализуема)
⊥ -> True (не реализуема)
⊥ -> False (не реализуема)
True -> ⊥
True -> True
True -> False
False -> ⊥
False -> True
False -> False
⊥ -> ⊥ (не реализуема)
⊥ -> True (не реализуема)
⊥ -> False (не реализуема)
t
ок, если ⊥ обозначать пустой тип, то при чем тут он? мы же вроде Bool обсуждали и функции на нем
тогда я запутался :с извините.
V
почему? если считать, что в Boolean включен боттом, то это
True -> ⊥
True -> True
True -> False
False -> ⊥
False -> True
False -> False
⊥ -> ⊥ (не реализуема)
⊥ -> True (не реализуема)
⊥ -> False (не реализуема)
True -> ⊥
True -> True
True -> False
False -> ⊥
False -> True
False -> False
⊥ -> ⊥ (не реализуема)
⊥ -> True (не реализуема)
⊥ -> False (не реализуема)
всего функций на 3-элементном множестве не 3*3, а 3^3, и да, не все из них реализуемы
t
почему 3-элементном? в задаче было "от Bool до Bool", т.е. не от двух аргументов
V
Bool = { True, False, ⊥ }
t
да, откуда тогда 27? чисто комбинаторно есть только 3*3 вариантов
t
было бы Bool -> Bool -> Bool, тогда да
V
да, откуда тогда 27? чисто комбинаторно есть только 3*3 вариантов
функций из n-элементного множества в m-элементное всего m^n
Oℕ
нет, комбинаторно X -> Y |Y| ^ |X| вариантов
Oℕ
у вас есть |X| ячеек для каждой из которых нужно определить значение |Y| поэтому со многих точек зрения X -> Y - это X- кратное произведение Y самого на себя
t
ок, если ⊥ обозначать пустой тип, то при чем тут он? мы же вроде Bool обсуждали и функции на нем
я так понял, что ⊥ является типом... объектом в категории. К нему всегда есть стрелка от любого другого типа, потому что любая функция может вместо одного из термов в результирующем типе "не вернуться", т.е. по факту иметь тип результата ⊥
V
почему? если считать, что в Boolean включен боттом, то это
True -> ⊥
True -> True
True -> False
False -> ⊥
False -> True
False -> False
⊥ -> ⊥ (не реализуема)
⊥ -> True (не реализуема)
⊥ -> False (не реализуема)
True -> ⊥
True -> True
True -> False
False -> ⊥
False -> True
False -> False
⊥ -> ⊥ (не реализуема)
⊥ -> True (не реализуема)
⊥ -> False (не реализуема)
ну вот в этом же сообщении вы используете этот символ как элемент Bool
t
нет, комбинаторно X -> Y |Y| ^ |X| вариантов
а, подождите, я, кажется, понял.
V
я так понял, что ⊥ является типом... объектом в категории. К нему всегда есть стрелка от любого другого типа, потому что любая функция может вместо одного из термов в результирующем типе "не вернуться", т.е. по факту иметь тип результата ⊥
тип функции известен статически. если функция не завершается, то она _возвращает_ значение ⊥, но тип у нее не меняется, он фиксирован
t
я совершенно упустил из виду, что результат функции зависит от аргумента