幻影类型背后的动机？

Question

Don Stewart 在大型演讲中的Haskell提到了Phantom Types:

data Ratio n = Ratio Double
1.234 :: Ratio D3

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

我读了他们关于他们的要点,但我不理解他们.另外,我在这个主题上阅读了Haskell Wiki.但我仍然错过了他们的观点.

使用幻影类型的动机是什么？

Answer 1

回答"使用幻影类型的动机是什么".有两点:

• 使无效状态无法代表,这在Aadit的答案中得到了很好的解释
• 携带类型级别的一些信息

例如,您可以通过长度单位标记距离:

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

这种方法特别简化Expr a了Aadit答案的例子:

{-# LANGUAGE GADTs #-}

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

值得指出的是,后者的变化需要不平凡的语言扩展(GADTs,DataKinds,KindSignatures),这可能不是在你的编译器的支持.Mu编译器 Don提到的情况可能就是这种情况.

Answer 2

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

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

两者的返回类型Nil和Cons是List a在默认情况下(这是广义的类型的所有列表a).

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

还要注意,这Nil是一个幻像构造函数(即它的返回类型不依赖于它的参数,在这种情况下是空的,但仍然是相同的).

因为Nil是一个幻像构造函数,我们可以专注Nil于我们想要的任何类型(例如Nil :: List Int或Nil :: List Char).

Haskell中的常规代数数据类型允许您选择数据构造函数的参数类型.例如,我们为Cons上面(a和List 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

如您所见,所有数据构造函数的返回类型都是一般化的.这是有问题的,因为我们知道,Number并且Increment必须返回一个Expr Int和Boolean和Not必须始终返回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

因此,当您想要专门化数据构造函数的返回类型时,幻像构造函数很有用,而幻像类型是构造函数都是幻像构造函数的数据类型.

请注意,数据构造函数喜欢Left并且Right也是幻像构造函数:

data Either a b = Left a | Right b

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

原因是尽管这些数据构造函数的返回类型确实取决于它们的参数,但它们仍然是一般化的,因为它们只部分依赖于它们的参数.

知道数据构造函数是否是幻像构造函数的简单方法:

出现在数据构造函数的返回类型中的所有类型变量是否也出现在数据构造函数的参数中？如果是的话,它不是幻像构造函数.

希望有所帮助.