Как я могу доказать эту теорему Хаскелла уровня типа?
Выбранный вывод называется байтовым объектом. Для его декодирования вам нужно сделать output.decode('utf-8').
Например:
output = b'\xe8\xbf\x99\xe7...'
unicode_output = output.decode('utf-8')
print(unicode_output)
выдаст нелатинские символы (я не могу включить его, потому что он считается как спам).
Другим способом сделать это в одной строке будет: print(b'\xe8\xbf\x99\xe7...'.decode('utf-8')).
Однако, если это не сработает, возможно, это связано с тем фактом, что ваш вывод не является байтовым объектом, но содержится внутри строки. Если это не сработает, то есть другое решение.
output = '\xe8\xbf\x99\xe7...'
exec('print(b\''+ output + '\'.decode(\'utf-8\'))')
Это должно быть в состоянии исправить. Надеюсь, у вас есть что-то полезное. Удачного дня!
1 ответ
Чтобы доказать это, просто начните с одной стороны уравнения и переписывайте, пока не дойдете до другой стороны. Мне нравится начинать с более сложной стороны.
when x :: Int,
Continuant (getUI (Continuant x))
-- ^^^^^^^^^^^^^^^^^^^^
-- by definition of getUI in Category Continuant Int
= Continuant x
Это было легко! Это считается доказательством (обратите внимание, формально не проверено - Haskell недостаточно силен, чтобы выразить доказательства на уровне терминов. Но это настолько тривиально, что в Агде это не стоило бы эталона).
Я был немного озадачен формулировкой этой аксиомы, так как она, кажется, довольно часто смешивает типы и термины. Пролистывая статью, кажется, что она предназначена для работы только с простым одним конструктором newtype, поэтому это смешение оправдано (все еще странно). В любом случае, похоже, что в статье нет класса Category, параметризованного на a: то есть вместо
class Category t a where ...
это будет
class Category t where ...
, что имеет больше смысла для меня то, что класс описывает полиморфные обертки, а не, возможно, другое описание того, как он обертывает каждый отдельный тип (тем более что кажется, что аксиома требует, чтобы реализация была одинаковой независимо от того, что a вы выберете!). [ 1111]