Haskell定理證明策略作為索引函子和單子

我正在嘗試按照這篇博客文章在 Haskell 中制作一種簡單的直覺定理證明語言。van Bakel 先生建議使用索引單子來進行證明狀態操作；這是索引 monad 的構建部分（相當于 的定義Control.Monad.Indexed）：

class IFunctor f where
  imap :: (a -> b) -> f j k a -> f j k b

class IFunctor m => IPointed m where
  ipure :: a -> m i i a

class IPointed m => IApplicative m where
  iap :: m i j (a -> b) -> m j k a -> m i k b

class IApplicative m => IMonad m where
  ibind :: (a -> m j k b) -> m i j a -> m i k b

ijoin :: IMonad m => m i j (m j k a) -> m i k a
ijoin = ibind id

infixr 1 =<<<
infixl 1 >>>=

(>>>=) :: IMonad m => m i j a -> (a -> m j k b) -> m i k b
m >>>= k = ibind k m

(=<<<) :: IMonad m => (a -> m j k b) -> m i j a -> m i k b
(=<<<) = ibind

我正在努力使用以下定義正確實體化這些類Tactic：

data Tactic i j a = Tactic ((a -> j) -> i)

開頭IFunctor：

instance IFunctor Tactic where
  imap f (Tactic g) = Tactic (\ h -> g (h . f))

-- f :: a -> b
-- g :: (a -> j) -> i
-- h :: b -> j

現在讓它指出：

instance IPointed Tactic where
  ipure a = Tactic (\ h -> h a)

很簡單。但是，我無法完全理解構建 applicative 和 monadic 實體。我對單子的猜測是

instance IMonad Tactic where
  ibind f (Tactic g) = Tactic (\ h -> imap g (imap h . f))

-- f :: a -> Tactic ((b -> k) -> j)
-- g :: (a -> j) -> i
-- h :: b -> k
-- RHS :: Tactic ((b -> k) -> i)

因為簽名似乎已簽出。不過，我完全被應用實體難住了。

instance IApplicative Tactic where
  iap (Tactic f) (Tactic g) = Tactic (\ h -> ???)

-- f :: ((a -> b) -> j) -> i
-- g :: (a -> k) -> j
-- h :: b -> k
-- RHS :: Tactic ((b -> k) -> i)

你有什么建議？

編輯：我得到了應用實體來作業

instance IApplicative Tactic where
  iap (Tactic f) (Tactic g) = Tactic (\ h -> f (\ x -> g (h . x)))

-- f :: ((a -> b) -> j) -> i
-- g :: (a -> k) -> j
-- h :: b -> k
-- RHS :: Tactic ((b -> k) -> i)
-- x :: a -> b, h . x :: a -> k

感謝 Li-Yao 對g簽名拼寫錯誤的提示，但我仍然堅持系結定義。

uj5u.com熱心網友回復：

提示：

• 評論中的型別有錯字g（編輯：現已修復）
• 孔的型別是???什么？（請參閱下面的更多詳細資訊）
• 另一種方法是使用 and 實作iap，與使用imapand實作相同ibind的方法(<*>)fmap(>>=)
• Tactic是 continuation monad 的索引版本type Cont r a = (a -> r) -> r，所以如果你熟悉它，實作是相同的。

您可以通過放置漏洞并查看編譯器的錯誤訊息來進行型別驅動編程。_

instance IMonad Tactic where
  ibind f (Tactic g) = Tactic _

-- error: Found hole: _ :: (b -> k) -> i

當孔具有函式型別時，從 lambda 開始總是安全的：

instance IMonad Tactic where
  ibind f (Tactic g) = Tactic (\h -> _)

-- error: Found hole: _ :: i
-- Relevant bindings include
--        h :: b -> k
--        g :: (a -> j) -> i
--        f :: a -> Tactic j k b

產生 an 的唯一方法i是應用于g某個論點。

instance IMonad Tactic where
  ibind f (Tactic g) = Tactic (\h -> g _)

-- error: Found hole: _ :: a -> j

又是一個功能。

instance IMonad Tactic where
  ibind f (Tactic g) = Tactic (\h -> g (\a -> _))

-- error: Found hole: _ :: j
-- Relevant bindings include
--        a :: a
--        h :: b -> k
--        g :: (a -> j) -> i
--        f :: a -> Tactic j k b

There is no obvious way to produce a j, but there is a way to use the a which we just introduced, with f :: a -> Tactic j k b (and upon closer inspection we see that it will in fact yield a j eventually). We can then pattern-match on the resulting Tactic to get some more data:

instance IMonad Tactic where
  ibind f (Tactic g) = Tactic (\h -> g (\a ->
    let Tactic p = f a in _))

-- error: Found hole: _ :: j
-- Relevant bindings include
--        p :: (b -> k) -> j
--        a :: a
--        h :: b -> k
--        g :: (a -> j) -> i
--        f :: a -> Tactic j k b

The final step is left as an exercise for the reader.

標籤：哈斯克尔 单子 定理证明

上一篇：Parsec的類折疊運算子

下一篇：哈斯克爾|如何將CSV檔案中的數字串列轉換為包含串列的串列