有沒有辦法限制可能的產品類型的實例？

讓我們假設這2和類型有沒有辦法限制可能的產品類型的實例？

data Currency = 
    | GBP 
    | EUR 
    | DKK 

data Country = 
    | DE 
    | AT 
    | DK 
    | UK

及以下產品類型

type CC = (Country, Currency)

現在即使所有這些國家都是歐盟的一部分（是的，從3000年親愛的軟件考古學家 - 英國曾經是歐盟的一部分;-)）他們有不同的貨幣（或不同）。所以我想限制的CC的可能值

(DE, EUR) 
(AT, EUR) 
(UK, GBP) 
(DK, DKK)

，並盡一切其他組合不可表達。
是否有可能在類型級別上表達這樣的東西？
如果不是，那麼精通Haskeller的方法會如何呢？

來源

2017-02-16 robkuz

什麼會使用這種類型級映射？正如英國所表明的那樣，它反映的並不是靜態的真實世界的數據。 – chepner

我認爲幾乎沒有數據是靜態的。如果我們在不太遙遠的將來解決火星問題，我們的日期系統和時間系統將不再適用。目前我有信心實施24/365。所以我使用上面的靜態表。如果想要實現一個可配置的模塊，那麼最後總會有一個判斷調用，不是嗎？ – robkuz

這可能是矯枉過正，但根據您所在的上下文，您可以使用GADT。對於至少您的貨幣沒有任何構造函數的信息，這非常重要。

{-# LANGUAGE GADTs, DataKinds #-} 

data Currency = GBP | EUR | DKK 

data Country c where 
    DE :: Country EUR 
    AT :: Country EUR 
    UK :: Country GBP 
    DK :: Country DKK

或者，變體，我認爲可能是不太有用的，但更接近問題

{-# LANGUAGE GADTs, DataKinds #-} 

data Currency = GBP | EUR | DKK 
data Country = DE | AT | DK | UK 

data CountryCurrency country currency where 
    DECC :: CountryCurrency DE EUR 
    ATCC :: CountryCurrency AT EUR 
    UKCC :: CountryCurrency UK GBP 
    DKCC :: CountryCurrency DK DKK

在沒有使用的情況下，這是很難說的，最好的方法是什麼。 :)

來源

2017-02-16 10:01:45 Alec

您的第二個實現不會編譯，因爲有'DE'，'AT'等重複名稱。 –

@DavidYoung謝謝！固定。 – Alec

[編輯：我忽略了一個事實，即OP在類型級別上尋求解決方案，用於編譯時檢查;我的回答沒有回答，但可以在類似的情況下一般是一個很好的選擇]

我相信這樣做的慣用方式是使用smart constructors。簡而言之：您可以在模塊中定義數據類型，並且不會導出「危險」數據構造函數（允許「非法」組合的構造函數）;相反，您可以導出一個只具有合法價值的功能。在你的情況：

module Money (CountryCurrency 
      , Country (..) 
      , Currency (..) 
      , cc 
      ) where 

data Currency = GBP | EUR | DKK deriving Show 

data Country = DE | AT | DK | UK deriving Show 

data CountryCurrency = CC Country Currency deriving Show 

cc :: Country -> Currency -> CountryCurrency 
cc DE EUR = CC DE EUR 
cc AT EUR = CC AT EUR 
cc UK GBP = CC UK GBP 
cc DK DKK = CC DK DKK 
cc _ _ = error "invalid country/currency combination"

cc是聰明的構造函數。然後，您可以進行有效的組合是這樣的：

*Main> cc DE EUR 
CC DE EUR 

*Main> cc UK GBP 
CC UK GBP

但你不能做違法的：

*Main> cc UK EUR 
*** Exception: invalid country/currency combination 
CallStack (from HasCallStack): 
    error, called at ./Money.hs:18:10 in main:Money

最重要的是，你不能使用數據構建器CC直接：

*Main> CC UK EUR 

<interactive>:26:1: error: 
    Data constructor not in scope: CC :: Country -> Currency -> t

來源

2017-02-16 14:44:29

我的目標是進行編譯時檢查。 – robkuz

@robkuz智能構造函數鏈接也可以對此進行說明。也許它會有所幫助。 –

我覺得'國家 - >貨幣 - >也許CountryCurrency'會更好。部分功能是邪惡的。 – user2297560

我爭議在於產品類型是表示這種映射的錯誤方式，而且這種類型不是檢查其一致性的好工具。（你如何確定你的類型是正確的映射？如果映射改變了，那麼你也需要改變類型。）

每個國家只有一種貨幣，貨幣是唯一由國家。聽起來更像一個功能，而不是一對。

currency :: Country -> Currency 
currency DE = EUR 
currency AT = EUR 
currency UK = GBP 
currency DK = DKK

來源

2017-02-16 17:53:17

有沒有辦法限制可能的產品類型的實例？

回答

相關問題