Мотивация за фантомными типами?

Question

презентация Haskell in the Large Дон Стюарт «s упоминается Фантом Типы:

data Ratio n = Ratio Double 
1.234 :: Ratio D3 

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

Я перечитал его пункты маркированного о них, но я их не понимаю. Кроме того, я прочитал Haskell Wiki по теме. Но я до сих пор не пропустил их.

Какова мотивация использования фантомного типа?

Answer 1

Чтобы ответить на вопрос «что такое мотивация использования фантомного типа». Существует две точки:

• сделать недопустимые состояния inrepresentable, которые хорошо описаны в 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 

И вы можете избежать Mars Climate Orbiter disaster:

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

В расстоянии случае мы можем отработать добавление, к примеру перевести в километры, если разные единицы участвуют. Но это не работает хорошо для валют, доля которых не является постоянным во времени и т.д.

---

И это можно использовать для GADTs, что вместо этого, что может быть более простой подход в некоторых ситуациях:

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

---

Такой подход особенно greately упрощает Expr a пример из Aadit's answer:

{-# 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), которые не могут быть поддержаны в вашем компилятор. Это может быть в случае с Му компилятор Дон упоминает.

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 

Причина в том, что хотя тип возврата этих конструкторах данных действительно зависят от их аргументов, но они все еще обобщенно, потому что они лишь частично зависят от их аргументов.

Простой способ узнать, если конструктор данных фантом конструктор:

ли все переменные типа, входящие в возвращаемый тип конструктора данных также появляться в аргументах конструктора данных? Если да, это не фантомный конструктор.

Надеюсь, что это поможет.

Answer 3

Для Ratio D3 конкретно мы используем такие богатые типы, чтобы управлять типом кода, таким образом, например, если у вас есть поле где-то типа Ratio D3, его редактор отправляется в текстовое поле, принимающее только числовые записи и показывающее точность 3 цифры. Это контрастирует, например, с newtype Amount = Amount Double, где мы не показываем десятичные цифры, но используем тысячи запятых и синтаксический ввод, например «10 м», как «10 000 000».

В базовом представлении, оба по-прежнему только Double s.