haskell Phantom类型背后的动机?

ny6fqffe  于 2023-11-18  发布在  其他
关注(0)|答案(3)|浏览(111)

Don Stewart的Haskell in the Large演示文稿中提到了 * 幻影类型 *:

data Ratio n = Ratio Double
1.234 :: Ratio D3

data Ask ccy = Ask Double
Ask 1.5123 :: Ask GBP

字符串
我读了他关于这些问题的要点,但我不明白。此外,我读了关于这个问题的Haskell Wiki。但我仍然没有理解他们的观点。
使用幻影类型的动机是什么?

yebdmbv4

yebdmbv41#

要回答“使用幻影类型的动机是什么”。有两点:

  • 使无效状态不可表示,这在Aadit's answer中有很好的解释。
  • 携带类型级别上的一些信息

例如,您可以使用长度单位标记距离:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

newtype Distance a = Distance Double
  deriving (Num, Show)

data Kilometer
data Mile

marathonDistance :: Distance Kilometer
marathonDistance = Distance 42.195

distanceKmToMiles :: Distance Kilometer -> Distance Mile
distanceKmToMiles (Distance km) = Distance (0.621371 * km)

marathonDistanceInMiles :: Distance Mile
marathonDistanceInMiles = distanceKmToMiles marathonDistance

字符串
你可以避免火星气候轨道器灾难:

>>> marathonDistanceInMiles
Distance 26.218749345

>>> marathonDistanceInMiles + marathonDistance

<interactive>:10:27:
    Couldn't match type ‘Kilometer’ with ‘Mile’
    Expected type: Distance Mile
      Actual type: Distance Kilometer
    In the second argument of ‘(+)’, namely ‘marathonDistance’
    In the expression: marathonDistanceInMiles + marathonDistance


这个“模式”有一些细微的变化。你可以使用DataKinds来拥有封闭的单位集:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}

data LengthUnit = Kilometer | Mile

newtype Distance (a :: LengthUnit) = Distance Double
  deriving (Num, Show)

marathonDistance :: Distance 'Kilometer
marathonDistance = Distance 42.195

distanceKmToMiles :: Distance 'Kilometer -> Distance 'Mile
distanceKmToMiles (Distance km) = Distance (0.621371 * km)

marathonDistanceInMiles :: Distance 'Mile
marathonDistanceInMiles = distanceKmToMiles marathonDistance


它的工作原理类似于:

>>> marathonDistanceInMiles
Distance 26.218749345

>>> marathonDistance + marathonDistance
Distance 84.39

>>> marathonDistanceInMiles + marathonDistance

<interactive>:28:27:
    Couldn't match type ‘'Kilometer’ with ‘'Mile’
    Expected type: Distance 'Mile
      Actual type: Distance 'Kilometer
    In the second argument of ‘(+)’, namely ‘marathonDistance’
    In the expression: marathonDistanceInMiles + marathonDistance


但是现在Distance只能以公里或英里为单位,我们不能在以后添加更多的单位。这在某些用例中可能有用。
我们还可以:

data Distance = Distance { distanceUnit :: LengthUnit, distanceValue :: Double }
   deriving (Show)


在距离的情况下,我们可以计算出加法,例如,如果涉及到不同的单位,则转换为公里。但是这对于 * 货币 * 并不适用,因为它的比率随着时间的推移而变化。
可以使用GADT来实现,在某些情况下这可能是更简单的方法:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}

data Kilometer
data Mile

data Distance a where
  KilometerDistance :: Double -> Distance Kilometer
  MileDistance :: Double -> Distance Mile

deriving instance Show (Distance a)

marathonDistance :: Distance Kilometer
marathonDistance = KilometerDistance 42.195

distanceKmToMiles :: Distance Kilometer -> Distance Mile
distanceKmToMiles (KilometerDistance km) = MileDistance (0.621371 * km)

marathonDistanceInMiles :: Distance Mile
marathonDistanceInMiles = distanceKmToMiles marathonDistance


现在我们知道单位也在价值层面上:

>>> marathonDistanceInMiles 
MileDistance 26.218749345


这种方法特别简化了Aadit's answerExpr a示例:

{-# LANGUAGE GADTs #-}

data Expr a where
  Number     :: Int -> Expr Int
  Boolean    :: Bool -> Expr Bool
  Increment  :: Expr Int -> Expr Int
  Not        :: Expr Bool -> Expr Bool


值得指出的是,后一种变体需要非平凡的语言扩展(GADTsDataKindsKindSignatures),这可能在您的编译器中不受支持。

bwleehnv

bwleehnv2#

使用幻影类型背后的动机是专门化数据构造函数的返回类型。例如,考虑:

data List a = Nil | Cons a (List a)

字符串
默认情况下,NilCons的返回类型都是List a(这适用于所有a类型的列表)。

Nil  ::                List a
Cons :: a -> List a -> List a
                       |____|
                          |
                    -- return type is generalized


还要注意,Nil是一个幻影构造函数(也就是说,它的返回类型不依赖于它的参数,在这种情况下是空的,但仍然是一样的)。
因为Nil是一个幻影构造函数,我们可以将Nil专门化为任何我们想要的类型(例如Nil :: List IntNil :: List Char)。
Haskell中的普通代数数据类型允许您选择数据构造函数的参数类型。例如,我们为上面的Cons选择了参数类型(aList a)。
然而,它不允许你选择数据构造函数的返回类型。返回类型总是泛化的。这对大多数情况都很好。但是,也有例外。例如:

data Expr a = Number     Int
            | Boolean    Bool
            | Increment (Expr Int)
            | Not       (Expr Bool)


数据构造函数的类型为:

Number    :: Int       -> Expr a
Boolean   :: Bool      -> Expr a
Increment :: Expr Int  -> Expr a
Not       :: Expr Bool -> Expr a


正如你所看到的,所有数据构造函数的返回类型都是通用的。这是有问题的,因为我们知道NumberIncrement必须总是返回Expr IntBooleanNot必须总是返回Expr Bool
数据构造函数的返回类型是错误的,因为它们太通用了。例如,Number不可能返回Expr a,但它确实返回了。这允许您编写类型检查器无法捕获的错误表达式。例如:

Increment (Boolean False) -- you shouldn't be able to increment a boolean
Not       (Number  0)     -- you shouldn't be able to negate a number


问题是我们不能指定数据构造函数的返回类型。
请注意,Expr的所有数据构造函数都是幻影构造函数(即它们的返回类型不依赖于它们的参数)。构造函数都是幻影构造函数的数据类型称为幻影类型。
请记住,像Nil这样的幻影构造函数的返回类型可以专门化为我们想要的任何类型。因此,我们可以为Expr创建智能构造函数,如下所示:

number    :: Int       -> Expr Int
boolean   :: Bool      -> Expr Bool
increment :: Expr Int  -> Expr Int
not       :: Expr Bool -> Expr Bool

number    = Number
boolean   = Boolean
increment = Increment
not       = Not


现在我们可以使用智能构造函数来代替普通构造函数,我们的问题就解决了:

increment (boolean False) -- error
not       (number  0)     -- error


因此,当你想专门化数据构造函数的返回类型时,幻影构造函数很有用,幻影类型是其构造函数都是幻影构造函数的数据类型。
注意,像LeftRight这样的数据构造函数也是幻影构造函数:

data Either a b = Left a | Right b

Left  :: a -> Either a b
Right :: b -> Either a b


原因是,虽然这些数据构造函数的返回类型确实依赖于它们的参数,但它们仍然是通用的,因为它们只部分依赖于它们的参数。
了解数据构造函数是否是幻影构造函数的简单方法:
所有出现在数据构造函数返回类型中的类型变量是否也出现在数据构造函数的参数中?如果是,它不是幻影构造函数。
希望能帮上忙。

2wnc66cl

2wnc66cl3#

对于Ratio D3,我们使用丰富的类型来驱动类型导向的代码,例如,如果您有一个类型为Ratio D3的字段,其编辑器将被分派到一个只接受数字输入并显示3位精度的文本字段。这与之相反,例如,对于newtype Amount = Amount Double,我们不显示十进制数字,但是使用千个逗号并将输入如'10m'解析为'10,000,000'。
在底层表示中,两者仍然只是Double s。

相关问题