如何在Haskell中編寫這個依賴類型的示例？

Question

假設我想表示具有常數c，一元函數符號f和謂詞P的一階語言的有限模型。我可以將載體表示爲列表m，該常數作爲m的元素，函數爲有序對m元件（其可以經由一個輔助函數ap被應用）的列表，和謂詞作爲滿足它的m的元素的列表：

-- Models (m, c, f, p) with element type a 
type Model a = ([a], a, [(a,a)], [a]) 

-- helper function application, assumes function is total 
ap :: Eq a => [(a,b)] -> a -> b 
ap ((x',y'):ps) x = if x == x' then y' else ap ps x 

我然後可以構建特定的模型和模型操作。細節是不是我的問題很重要，只是類型的（但我已經包括了定義，所以你可以看到那裏的類型約束來自於）：

unitModel :: Model() 
unitModel = ([()],(), [((),())], []) 

cyclicModel :: Int -> Model Int 
cyclicModel n | n > 0 = ([0..n-1], 0, [(i, (i+1)`mod`n) | i<-[0..n-1]], [0]) 

-- cartesian product of models 
productModel :: (Eq a, Eq b) => Model a -> Model b -> Model (a,b) 
productModel (m1, c1, f1, p1) (m2, c2, f2, p2) = (m12, c12, f12, p12) where 
    m12 = [(x1,x2) | x1 <- m1, x2 <- m2] 
    c12 = (c1, c2) 
    f12 = [(x12, (ap f1 (fst x12), ap f2 (snd x12))) | x12 <- m12] 
    p12 = [x12 | x12 <- m12, elem (fst x12) p1 && elem (snd x12) p2] 

-- powerset of model (using operations from Data.List) 
powerModel :: (Eq a, Ord a) => Model a -> Model [a] 
powerModel (m, c, f, p) = (ms, cs, fs, ps) where 
    ms = subsequences (sort m) -- all subsets are "normalized" 
    cs = [c] 
    fs = [(xs, nub (sort (map (ap f) xs))) | xs <- ms] -- "renormalize" the image of f 
    ps = [xs | xs <- ms, elem c xs] 

現在，我想給名字所有的這些模型：

data ModelName = UnitModel 
       | CyclicModel Int 
       | Product ModelName ModelName 
       | Power ModelName 
       deriving (Show, Eq) 

最後，我想編寫此代碼，每個名稱映射到模型，可以名稱：

model_of UnitModel = unitModel 
model_of (CycleModel n) = cycleModel n 
model_of (Product m1 m2) = productModel (model_of m1) (model_of m2) 
model_of (Power m1) = powerModel (model_of m1) 

我已經嘗試了許多方法來使這個工作，在定義ty的意義因此我可以使用這個model_of的定義，包括使用幻像類型，GADT和類型族 - 但還沒有找到一種方法來實現它。 （但是，再次，我是Haskell的新手。）可以這樣做嗎？我應該怎麼做？

Answer 1

通過對ModelName使用GADT，可以將給定的名稱與生成的模型的類型參數相關聯。這裏是讓你的model_of編譯所需的內容：

{-# LANGUAGE GADTs #-} 

data ModelName t where 
    UnitModel :: ModelName() 
    CyclicModel :: Int -> ModelName Int 
    Product  :: (Eq a, Eq b) => ModelName a -> ModelName b -> ModelName (a, b) 
    Power  :: (Ord a) => ModelName a -> ModelName [a] 

model_of :: ModelName t -> Model t 
model_of UnitModel  = unitModel 
model_of (CyclicModel n) = cyclicModel n 
model_of (Product m1 m2) = productModel (model_of m1) (model_of m2) 
model_of (Power m1)  = powerModel (model_of m1) 

編輯：正如你注意到沒有，在正常deriving條款不與GADTs工作，但事實證明StandaloneDeriving作品就好了。

{-# LANGUAGE StandaloneDeriving #-} 

deriving instance Show (ModelName t) 
deriving instance Eq (ModelName t) 

但是請注意，該Eq實例是在這種情況下，一個有點無厘頭，因爲類型級允許你只比較同類型的值，但不同的構造函數產生實質上的不同類型的值。因此，舉例來說，下面甚至沒有類型檢查：

UnitModel == CyclicModel 

因爲UnitModel和CyclicModel有不同的類型（分別爲ModelName()和ModelName Int）。對於您需要刪除的附加類型信息出於某種原因，你可以使用一個包裝類如

data Some t where 
    Some :: t a -> Some t 

，你可以得到如情況一個Eq實例Some ModelName手動：

{-# LANGUAGE FlexibleInstances #-} 

instance Eq (Some ModelName) where 
    Some UnitModel == Some UnitModel 
     = True 

    Some (CyclicModel n) == Some (CyclicModel n') 
     = n == n' 

    Some (Product m1 m2) == Some (Product m1' m2') 
     = Some m1 == Some m1' && Some m2 == Some m2' 

    Some (Power m1) == Some (Power m1') 
     = Some m1 == Some m1' 

    _ == _ = False