haskell 基于上下文选择类型类示例(再次)

smdncfj3 于 2022-11-24 发布在其他

关注(0)|答案(3)|浏览(155)

好吧，这个主题已经讨论了很多次，但由于Haskell的发展，让我们再次考虑它，看看我们可以在当代Haskell（当代我的意思是GHC 9.0 - 9.2）做什么。
首先，让我通过一个例子来说明这个问题。假设我们有一个函数，它确定存储给定类型的值所需的字节数。我们可以有这个函数的两个示例：一个用于固定大小的数据类型，另一个用于可变大小的数据类型。例如，Int32是固定大小的，无论其值如何，总是需要4个字节来存储。但data C = A Int32 | B Int32 Int32可以被视为可变大小的，因为在A构造函数的情况下，它可能需要4个字节来存储，而在B构造函数的情况下，它可能需要8个字节来存储。为此，自然要有两个类：
1.固定大小值的类。注意值本身不是必需的，我们可以使用Proxy作为参数来确定大小。

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

1.可变大小值的类。该函数采用一个值来确定大小。

class VariableSize a where 
  variableSize :: a -> Int

现在，假设我们要定义一个函数来确定一个值列表的大小。列表中的值可以是固定大小的，也可以是可变大小的。因此，很自然地有两个函数：
1.一个用于固定大小值的列表。

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

1."其他"，表示大小可变的值的列表。

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。基本思想是定义反映上下文的类型级 predicate ，并使用它来选择使用多参数类型类和重叠示例的示例。在这种情况下，Haskell将能够基于类型参数选择更具体的示例。"更具体"是指匹配类型级 predicate 。
所提出的方法可以根据条件分为三组。
1.使用封闭的类型族来定义类型级 predicate （根据维基页面的"解决方案3"）。这不是一个可用的方法，因为它将不允许用户为自定义数据类型定义示例。我不会进一步讨论它。
1.将 predicate 定义为一个单独的类型类，为 predicate 定义默认的（回退）可重叠示例（根据维基页面的"解决方案1"）。这是一个可行的方法，但它要求用户为 predicate 维护额外的示例。
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]]

在我看来，这种方法是最方便的用户方式。仍然需要单独的类型级 predicate 工具，用户仍然可以通过显式定义如下内容来搞砸：

class FixedSize UserType where
  type FixedSized UserType = 'False

但在使用默认值时，它可以正常工作。
然而，它需要不连贯的示例。我害怕不连贯的示例。因为Hasllkel文档字面上说，在不连贯的示例的情况下，编译器可以自由选择它想要的任何示例，这看起来是不可预测的。现在我可能会做一件坏事，在一个帖子中问4个问题，但它们都是相关的：
1.为什么这里需要不一致的示例？ListSize 'True [a]不是正好与ListSize any [a]重叠，并且可以在第一个参数求值为True时被选取吗？
1.有没有办法破解这个代码？我的意思是，当FixedSize a在作用域中时，让编译器选择ListSize any [a]（可变大小的元素代码）？
1.这些示例真的不一致吗？可能编译器无法证明一致性，那么如何手动证明一致性呢？
1.在现代的Haskell中有没有一种完全不同的方法来解决这个问题？我所说的问题是指上面的一个部分例子，在编译时根据值的类型选择一个合适的函数来确定值列表的大小。

haskell

来源：https://stackoverflow.com/questions/74479429/selecting-a-type-class-instance-based-on-the-context-once-again

3条答案

按热度按时间

4urapxun1#

我将集中在具体的例子上，希望下面提出的一些解决方案也适用于你所想到的一般情况。
不过，有一个总的主题是：我们避免了有两个不同的类可供选择。
简单的基本方法
如果大小既可以是固定的也可以是可变的，我们可以使用求和类型来表示这两种情况。

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

本质上，我们将两个类合并为一个类：固定大小类型和可变大小类型的类现在只有一个。在类型级别，我们可以使用类型族F a区分这两种情况，而在术语级别，我们可以使用单例which @a区分这两种情况。

赞(0）回复(0）举报 2022-11-24

kqhtkvqz2#

这听起来像是if-instance的用法。
它允许你根据约束是否满足来进行分支，显然这是不安全的，因为它违反了开放世界的假设（参见reddit post）。
如果您声称您的类是互斥的，那么您应该能够安全地编写

{-# 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)

赞(0）回复(0）举报 2022-11-24

kmbjn2e33#

一种可能性是为容器的大小提供一个额外的类，以及与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

(If这感觉有点像是对列表的一种特殊情况，让我鼓励你，这与几十年来一直运行良好的标准库showList非常相似，因此这是它毕竟可以覆盖相当多领域的一些证据!）

赞(0）回复(0）举报 2022-11-24

我来回答

haskell 基于上下文选择类型类示例(再次)

3条答案

利用GADT

相关问题

热门标签

最新问答