好吧，這個話題已經被討論過很多次了，但是既然 Haskell 不斷發展，讓我們再考慮一下它，看看我們可以在當代的 Haskell 中做些什么（當代的我指的是 GHC 9.0 - 9.2）。

拳頭讓我通過一個例子來說明問題。假設我們有一個函式來確定存盤給定型別的值所需的位元組數。我們可以有此函式的兩個實體：一個用于固定大小的資料型別，另一個用于可變大小的資料型別。例如Int32，它是固定大小的，無論它的值如何，總是需要 4 個位元組來存盤。但是data C = A Int32 | B Int32 Int32可以被認為是可變大小的，因為在建構式的情況下可能需要 4 個位元組來存盤，而在A建構式的情況下可能需要 8 個位元組B。為此有兩個類是很自然的：

固定大小值的類。請注意，值本身不是必需的，我們可以將Proxy其用作引數來確定大小。

class FixedSize a where 
  fixedSize :: p a -> Int

可變大小值的類。該函式采用一個值來確定大小。

class VariableSize a where 
  variableSize :: a -> Int

現在假設我們要定義一個函式來確定值串列的大小。串列中的值可以是固定大小的，也可以是可變大小的。所以自然有兩個功能：

一個用于固定大小的值串列。

listSize :: (FixedSize a) => [a] -> Int
listSize _ = (* fixedSize (Proxy @a) ) . length

其他用于可變大小值的串列。

listSize :: (VariableSize a) => [a] -> Int
listSize = sum . map variableSize

然而，不可能使用天真的方法，以下基本上不會編譯：

class Size a where 
  size :: a -> Int

instance (FixedSize a) => Size [a] where
  size = _ = (* fixedSize (Proxy @a) ) . length

instance (VariableSize a) => Size [a] where
  size = sum . map variableSize

發生這種情況是因為 Haskell 在選擇實體時依賴于型別，而不依賴于背景關系。有一些技巧可以克服此處描述的此限制：https ://wiki.haskell.org/GHC/AdvancedOverlap 。基本思想是定義反映背景關系的型別級謂詞，并使用它來選擇使用多引數型別類和重疊實體的實體。在這種情況下，Haskell 將能夠根據型別引數選擇更具體的實體。“更具體”是指匹配型別級別的謂詞。

所提出的方法可以有條件地分為三組。

使用封閉型別族來定義型別級謂詞（根據 wiki 頁面的“解決方案 3”）。這是不可用的方法，因為它將不允許用戶為自定義資料型別定義實體。我不會進一步討論它。
將謂詞定義為單獨的型別類，為謂詞定義默認（回退）可重疊實體（根據 wiki 頁面的“解決方案 1”）。這是可行的方法，但它要求用戶為謂詞維護額外的實體。
使用開放式系列（“解決方案 2”）。我想討論一下這種方法的略微修改版本。

class Size a where 
  size :: a -> Int

class FixedSize a where
  type FixedSized a :: Bool
  type FixedSized a = 'True
  fixedSize :: p a -> Int

#include "MachDeps.h"
instance FixedSize Int where
  fixedSize _ = SIZEOF_HSINT

class ListSize (isElemFixed :: Bool) a where
  listSize :: p isElemFixed -> a -> Int

instance (ListSize (FixedSized a) [a]) => Size [a] where
  size = listSize $ Proxy @(FixedSized a)

instance (FixedSize a) => ListSize 'True [a] where
  listSize _ = trace "elem size is fiхed" . (* fixedSize (Proxy @a) ) . length

instance {-# INCOHERENT #-} (Size a) => ListSize any [a] where
  listSize _ = trace "elem size is variable" . sum . map size

test1 = size [1::Int,2,3]

test2 = size [[1::Int], [2,3,4]]

這種方法對我來說似乎是最方便的用戶方式。單獨的型別級謂詞工具仍然是必需的，用戶仍然可以通過明確定義這樣的東西來搞砸：

class FixedSize UserType where
  type FixedSized UserType = 'False

但它在使用默認值時按預期作業。

但是，它需要不連貫的實體。而且我害怕不連貫的情況。因為 Hasllkel 檔案 leterelly 說，在不連貫的實體的情況下，編譯器可以自由選擇它想要的任何看起來不可預測的實體。現在我可能會在一篇文章中問 4 個問題，但它們都相關：

為什么這里需要不連貫的實體？當第一個引數ListSize 'True [a]評估ListSize any [a]為?True
有沒有辦法破解這段代碼？我的意思是，讓編譯器在范圍內選擇ListSize any [a]（可變大小的 elem 代碼）FixedSize a？
這些實體真的不連貫嗎？可能編譯器無法證明一致性，那么如何手動證明呢？
在現代 Haskell 中是否有完全不同的方法來解決這個問題？我所說的問題是指上面的部分示例，選擇一個適當的函式來根據編譯時值的型別確定值串列的大小。

uj5u.com熱心網友回復：

這聽起來像是if-instance的用法。

它允許您根據是否滿足約束進行分支，顯然這不安全，因為它違反了開放世界的假設（請參閱reddit 帖子）。

如果您聲稱您的類是互斥的，那么您應該能夠安全地撰寫

{-# OPTIONS_GHC -fplugin=IfSat.Plugin #-}

import Data.Constraint.If ( type (||) (dispatch) )

instance FixedSize a || VariableSize a => Size [a] where
  size :: [a] -> Int
  size as = dispatch fixed variable where

    fixed :: FixedSize a => Int
    fixed = fixedSize (Proxy @a) * length as

    variable :: VariableSize a => Int
    variable = sum (map variableSize as)

uj5u.com熱心網友回復：

我將專注于具體示例。希望下面提出的一些解決方案也適用于您想到的一般情況。

不過，有一個普遍的主題是：我們避免有兩個不同的類別可供選擇。

簡單、基本的方法

如果大小可以是固定的或可變的，我們可以使用求和型別來表示這兩種情況。

data Scale a = Fixed Int | Variable (a -> Int)

class Size a where
   scale :: Scale a

instance Size Int where
   scale = Fixed 4

instance Size a => Size [a] where
   scale = case scale @a of
      Fixed n    -> Variable (\xs -> n * length xs)
      Variable s -> Variable (\xs -> sum $ map s xs)

size :: forall a. Size a => a -> Int
size x = case scale @a of
   Fixed n    -> n
   Variable s -> s x

利用 GADT

我們首先列舉兩種情況：

data Sized = Fixed | Variable

-- associated singleton
data SSized (s :: Sized) where
   SFixed    :: SSized 'Fixed
   SVariable :: SSized 'Variable

然后我們使用型別族來驅動兩種不同的型別。

type family Scale s a where
   Scale Fixed    _ = Int
   Scale Variable a = a -> Int

class Size a where
   type F a :: Sized
   which :: SSized (F a)
   scale :: Scale (F a) a

請注意該類還如何提供單例。然后我們可以實體化這個類。

instance Size Int where
   type F Int = Fixed
   which = SFixed
   scale = 4

instance Size a => Size [a] where
   type F [a] = Variable
   which = SVariable
   scale xs = case which @a of
      SFixed    -> scale @a * length xs
      SVariable -> sum $ map (scale @a) xs

size :: forall a. Size a => a -> Int
size x = case which @a of
   SFixed    -> scale @a
   SVariable -> scale @a x

本質上，我們將兩個類合二為一：固定大小和可變大小型別的類現在只是一個。在型別級別，我們可以使用 type family 區分這兩種情況F a，而在術語級別，我們可以使用 singleton 區分這兩種情況which @a。

uj5u.com熱心網友回復：

一種可能性是為容器的大小提供一個額外的類，以及與deriving. 用戶仍然需要為這個新類撰寫一個實體，但這將是一行很短的代碼。像這樣：

class ContainerSize a where
    containerSize :: Foldable f => f a -> Int

newtype FixedElement a = FixedElement a
instance FixedSize a => ContainerSize (FixedElement a) where
    containerSize c = fixedSize @a * length c

newtype VariableElement a = VariableElement { getVE :: a }
instance VariableSize a => ContainerSize (VariableElement a) where
    containerSize c = sum (variableSize . getVE <$> c)

instance ContainerSize a => VariableSize [a] where
    variableSize = containerSize

現在，當用戶以前會寫類似

instance FixedSize X where ...
instance VariableSize Y where ...

他們現在添加行

deriving instance ContainerSize X via FixedElement X
deriving instance ContainerSize Y via VariableElement Y

（如果這感覺有點像串列的特例 hack，讓我鼓勵你，這與標準庫中已經運行了幾十年的東西非常相似showList，所以這是一些證據表明它可以涵蓋很多畢竟是地面！）

轉載請註明出處，本文鏈接：https://www.uj5u.com/yidong/536673.html

標籤：哈斯克尔类型类类型级计算

上一篇：xor=(/=)是什么意思？

下一篇：Haskell為串列中的專案提供索引

根據背景關系選擇型別類實體（再次）

簡單、基本的方法

利用 GADT