Печать церковных логических выражений - PullRequest
Новая
       39

Печать церковных логических выражений

0 голосов
/ 09 марта 2019

Следующий код предназначен для печати церковного кодирования логических значений как Bool: 

{-#LANGUAGE FlexibleInstances #-}

instance Show (t -> t -> t) where
  show b = show $ b True False

, которое приводит к этой ошибке: 

<interactive>:4:21: error:
• Couldn't match expected type ‘t’ with actual type ‘Bool’
  ‘t’ is a rigid type variable bound by
    the instance declaration at <interactive>:3:10-27
• In the first argument of ‘b’, namely ‘True’
  In the second argument of ‘($)’, namely ‘b True False’
  In the expression: show $ b True False
• Relevant bindings include
    b :: t -> t -> t (bound at <interactive>:4:8)
    show :: (t -> t -> t) -> String (bound at <interactive>:4:3)

Как заставить это работать?

1 Ответ

5 голосов
/ 09 марта 2019

Проблема в том, что show :: (t -> t -> t) -> String должно работать для любой функции, работающей с любым типом t. Вы предполагаете, что t является логическим значением, которое недопустимо, потому что (согласно GHC) «t является переменной жесткого типа» и не может быть объединено со специализированным типом.

Одним из возможных решений будет специализация вашего экземпляра на Bool (необходимо FlexibleInstances) 

{-#LANGUAGE FlexibleInstances #-}

instance Show (Bool -> Bool -> Bool) where
  show b = show $ b True False

Но это уменьшит общность логики вашей Церкви.

Невозможно определить гибкое решение, которое будет работать с любым типом, потому что вам понадобится два представителя этого типа, которые описали бы случаи true и false , и там такие типы, как Void, которые не имеют (определенных) значений.

Идея, которая приходит мне в голову и является достаточно универсальной, состоит в том, чтобы добавить еще несколько классовых ограничений к t: 

{-#LANGUAGE FlexibleInstances #-}
import Data.Boolean

instance (Show t, Boolean t) => Show (t -> t -> t) where
  show b = show $ b true false

Класс Boolean собирает типы, которые в некоторых терминах могут пониматься как логические значения. Например для Bool: 

instance Boolean Bool where
  true = True
  false = False
  notB = not
  (||*) = (||)
  (&&*) = (&&)

И теперь мы можем гарантировать, что

  • t это то, что вы можете на самом деле show
  • Существует как минимум два допустимых и разных значения типа t, которые отображаются как true и false

Каковы обязательные обстоятельства, чтобы реально иметь возможность show функционировать такой подписью таким образом.

ВАЖНО

Следующий пример не будет работать: 

show (true :: (Show t, Boolean t) => t -> t -> t)

Проблема в том, что проверщик типов не будет угадывать, какой t у вас будет здесь. Это решение предоставляет действительный и рабочий экземпляр, но только для полностью созданных экземпляров типов. Если вы получите ошибку неоднозначности, вам нужно будет указать, что такое t: 

show (true :: Bool -> Bool -> Bool)
>>> "True"

show (true :: Int -> Int -> Int)  -- assuming Boolean instance
>>> "1"

EDIT

Еще одна идея была упомянута в комментариях. Решение будет заключаться в том, чтобы обернуть вашу Церковь логическим Rank2Type: 

{-# LANGUAGE Rank2Types #-}

newtype ChBool = ChBool (forall t. t -> t -> t)

Что позволит t быть любым типом, независимым от контекста. Тогда вы можете определить случайный экземпляр следующим образом: 

instance Show ChBool where
  show (ChBool f) = show $ f True False
...