Prelude モジュールを読む (7) Data.HeytingAlgebra, Data.BooleanAlgebra

Prelude モジュールを読む (7) Data.HeytingAlgebra, Data.BooleanAlgebra

Prelude モジュールは purescript-prelude パッケージで定義されているモジュールです。

今回は以下の2つのモジュールを確認します。

  • Data.HeytingAlgebra
  • Data.BooleanAlgebra

歴史的経緯は以下の issue や PR が参考になりました。

purescript

purescript-prelude パッケージ

Data.HeytingAlgebra

この型クラスはHaskellには無いですね。

PureScript Haskell
HeytingAlgebra 型クラス -

HeytingAlgebra 型クラス, (&&), (||)

class HeytingAlgebra a where  
  ff :: a  
  tt :: a  
  implies :: a -> a -> a  
  conj :: a -> a -> a  
  disj :: a -> a -> a  
  not :: a -> a  

infixr 3 conj as &&  
infixr 2 disj as ||  

Boolean インスタンス

ただのブール代数ですかね。

instance heytingAlgebraBoolean :: HeytingAlgebra Boolean where  
  ff = false  
  tt = true  
  implies a b = not a || b  
  conj = boolConj  
  disj = boolDisj  
  not = boolNot  

foreign import boolConj :: Boolean -> Boolean -> Boolean  
foreign import boolDisj :: Boolean -> Boolean -> Boolean  
foreign import boolNot :: Boolean -> Boolean  

exports.boolConj = function (b1) {  
  return function (b2) {  
    return b1 && b2;  
  };  
};  

exports.boolDisj = function (b1) {  
  return function (b2) {  
    return b1 || b2;  
  };  
};  

exports.boolNot = function (b) {  
  return !b;  
};  

Unit インスタンス

何に使うのか全くわからない・・・。

instance heytingAlgebraUnit :: HeytingAlgebra Unit where  
  ff = unit  
  tt = unit  
  implies _ _ = unit  
  conj _ _ = unit  
  disj _ _ = unit  
  not _ = unit  

(->) インスタンス

instance heytingAlgebraFunction :: HeytingAlgebra b => HeytingAlgebra (a -> b) where  
  ff _ = ff  
  tt _ = tt  
  implies f g a = f a `implies` g a  
  conj f g a = f a && g a  
  disj f g a = f a || g a  
  not f a = not (f a)  

これは少し気になるので型をチェックしておきます。

ff :: a -> b  
tt :: a -> b  
implies :: (a -> b) -> (a -> b) -> (a -> b)  
conj :: (a -> b) -> (a -> b) -> (a -> b)  
disj :: (a -> b) -> (a -> b) -> (a -> b)  
not :: (a -> b) -> (a -> b)  

HeytingAlgebra b のクラス制約がついているため、例えば (a -> Bool) であれば ff _ = false という感じで特殊化されるんですね。

使い道は・・・思いつかない・・・。

Record インスタンス

Record のインスタンスはいつも他とちょっと違うんですよね。レコードについて調べた時に振り返ることにします。

instance heytingAlgebraRecord :: (RL.RowToList row list, HeytingAlgebraRecord list row row) => HeytingAlgebra (Record row) where  
  ff = ffRecord  (RLProxy :: RLProxy list) (RProxy :: RProxy row)  
  tt = ttRecord  (RLProxy :: RLProxy list) (RProxy :: RProxy row)  
  conj = conjRecord  (RLProxy :: RLProxy list)  
  disj = disjRecord  (RLProxy :: RLProxy list)  
  implies = impliesRecord  (RLProxy :: RLProxy list)  
  not = notRecord  (RLProxy :: RLProxy list)  

Data.BooleanAlgebra

この型クラスも無いですね。

PureScript Haskell
BooleanAlgebra 型クラス -

BooleanAlgebra

クラス制約だけです。

class HeytingAlgebra a <= BooleanAlgebra a  

感想

次回でラストの予定です。

進捗

  • Control.Applicative
  • Control.Apply
  • Control.Bind
  • Control.Category
  • Control.Monad
  • Control.Semigroupoid
  • Data.Boolean
  • Data.BooleanAlgebra
  • Data.Bounded
  • Data.CommutativeRing
  • Data.DivisionRing
  • Data.Eq
  • Data.EuclideanRing
  • Data.Field
  • Data.Function
  • Data.Functor
  • Data.HeytingAlgebra
  • Data.Monoid
  • Data.NaturalTransformation
  • Data.Ord
  • Data.Ordering
  • Data.Ring
  • Data.Semigroup
  • Data.Semiring
  • Data.Show
  • Data.Unit
  • Data.Void