等式約束

Question

比方說，我有以下幾點：

type family TF a b 

我可以寫這樣的事情

type instance TF Int t = (t ~ (x,y)) => (Int,x,y) 

的也許傻的例子。

這個問題是沿着同一主題的接受這個問題的答案：Haskell: Equality constraint in instance

我想匹配，即使我不知道第二個參數是那一雙迫使第二個參數類型實例成對（如果這不成功，將導致編譯錯誤）。

Answer 1

您可以使用新的TypeError功能在GHC 8.0中做到這一點，具體取決於「強制第二個參數是一對」的含義。

*Pair> let x = x in x :: TF Int Bool 

<interactive>:9:1: error: 
    • Fst: expected a pair, but got Bool 
    • When checking the inferred type 
     it :: (Int, (TypeError ...), (TypeError ...)) 

然而，這並沒有真正「力」的說法是一種對任：

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-} 

module Pair where 

import GHC.TypeLits 

type family Fst p where 
    Fst (x, y) = x 
    Fst _t = TypeError (Text "Fst: expected a pair, but got " :<>: ShowType _t) 

type family Snd p where 
    Snd (x, y) = y 
    Snd _t = TypeError (Text "Snd: expected a pair, but got " :<>: ShowType _t) 

type family TF a b 
type instance TF Int t = (Int, Fst t, Snd t) 

現在，如果你嘗試應用TF Int到非元組，你應該得到一個編譯錯誤不止是致電fromJust「強制」其論點形式爲Just x。它實際上是在類型級別上使用部分函數編程的。

家庭應用類型的良構完全由類型家庭的種類決定，一對(x, y)與具有相同種類，如Bool。你不能簡單地通過寫下一個類型系列的應用程序來奇蹟般地產生約束。如果您想在類型級別獲得約束，則必須將其寫入=>的左側。

在鏈接的問題中，CanFilter (b -> c) a已經是一個約束，所以它可能暗示b ~ c。