Как я могу доказать эту теорему Хаскелла уровня типа? - PullRequest
Новая
       6

Как я могу доказать эту теорему Хаскелла уровня типа?

0 голосов
/ 18 января 2019

Относительно Листинга 1 , как бы я смог доказать аксиому уровня типа

(t a) = (t (getUI (t a)))

имеет

Листинг 1 

    data Continuant a = Continuant a  deriving (Show,Eq)

    class UI a where

    instance UI Int where

    class Category t  where
      getUI :: (UI a) => (t a) -> a

   instance Category Continuant where
     getUI (Continuant a) = a

     -- Does axiom (t a) = (t (getUI(t a))) holds for given types?
     test :: Int -> Bool
     test x =  (Continuant x) == (Continuant (getUI (Continuant x)))

Код основан на бумаге , где указано:

Для всех реализаций getUI может потребоваться, чтобы аксиома (t a) = (t (getUI (t a))). Это должно быть подтверждено для каждого конкретного объявления экземпляра класса типа. Для конечных типов это может быть сделано программой, которая перечисляет все возможности. Для бесконечного Типы это должно быть сделано вручную через доказательства по индукции.

Моя текущая интуиция заключается в том, что функция test в некотором роде удовлетворяет аксиоме, но я не думаю, что это составляет доказательство.

Этот вопрос следует из предыдущего вопроса .

1 Ответ

0 голосов
/ 18 января 2019

Чтобы доказать это, просто начните с одной стороны уравнения и переписывайте, пока не дойдете до другой стороны. Мне нравится начинать с более сложной стороны. 

when x :: Int,

Continuant (getUI (Continuant x))
    --      ^^^^^^^^^^^^^^^^^^^^
    -- by definition of getUI in Category Continuant Int
    = Continuant x

Это было легко! Это считается доказательством (обратите внимание, формально не проверено - Haskell не достаточно силен, чтобы выразить доказательства на уровне терминов. Но это настолько тривиально, что в Агде не стоит эталона).

Я был немного озадачен формулировкой этой аксиомы, так как она, кажется, довольно часто смешивает типы и термины. Пролистывая статью, кажется, что она предназначена только для простого однократного конструктора newtype s, поэтому это смешивание оправдано (все еще странно). В любом случае, похоже, что у бумаги нет класса Category, параметризованного на a: то есть вместо 

class Category t a where ...

это будет 

class Category t where ...

, что для меня имеет больше смысла, так как класс описывает полиморфные обертки, а не, возможно, другое описание того, как он обертывает каждый отдельный тип (особенно, если учесть, что аксиома требует, чтобы реализация была одинаковой независимо от того, что a Вы выбираете!).

...