haskell - ¿Motivación detrás de los tipos de fantasmas?

phantom-types

Question

Haskell de Don Stewart en la presentación de Large mencionó los Phantom Types :

data Ratio n = Ratio Double
1.234 :: Ratio D3

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

Leí sus puntos sobre ellos, pero no los entendí. Además, leí el Wiki de Haskell sobre el tema. Sin embargo, todavía estoy perdiendo su punto.

¿Cuál es la motivación para usar un tipo fantasma?

Answer 1

La motivación detrás del uso de los tipos fantasma es especializar el tipo de retorno de los constructores de datos. Por ejemplo, considere:

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

El tipo de retorno de Nil y Cons es List a por defecto (que está generalizado para todas las listas de tipo a ).

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

También tenga en cuenta que Nil es un constructor fantasma (es decir, su tipo de retorno no depende de sus argumentos, en este caso, de manera imprecisa, pero de todos modos es el mismo).

Como Nil es un constructor fantasma, podemos especializar Nil en cualquier tipo que deseemos (por ejemplo, Nil :: List Int o Nil :: List Char ).

Los tipos de datos algebraicos normales en Haskell le permiten elegir el tipo de argumentos de un constructor de datos. Por ejemplo, elegimos el tipo de argumentos para los Cons anteriores ( a y List a ).

Sin embargo, no le permite elegir el tipo de devolución de un constructor de datos. El tipo de devolución siempre es generalizado. Esto está bien para la mayoría de los casos. Sin embargo, hay excepciones. Por ejemplo:

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

El tipo de constructores de datos son:

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

Como puede ver, el tipo de devolución de todos los constructores de datos está generalizado. Esto es problemático porque sabemos que Number e Increment siempre deben devolver un Expr Int y Boolean y Not siempre debe devolver un Expr Bool .

Los tipos de devolución de los constructores de datos son incorrectos porque son demasiado generales. Por ejemplo, Number no puede devolver un Expr a pero lo hace. Esto le permite escribir expresiones incorrectas que el verificador de tipos no captará. Por ejemplo:

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

El problema es que no podemos especificar el tipo de devolución de los constructores de datos.

Observe que todos los constructores de datos de Expr son constructores fantasmas (es decir, su tipo de devolución no depende de sus argumentos). Un tipo de datos cuyos constructores son todos constructores fantasmas se llama tipo fantasma.

Recuerde que el tipo de devolución de constructores fantasmas como Nil puede estar especializado en cualquier tipo que deseemos. Por lo tanto, podemos crear constructores inteligentes para Expr siguiente manera:

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

Ahora podemos usar los constructores inteligentes en lugar de los constructores normales y nuestro problema está resuelto:

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

Así que los constructores fantasmas son útiles cuando se quiere especializar el tipo de retorno de un constructor de datos y los tipos fantasmas son tipos de datos cuyos constructores son todos constructores fantasmas.

Tenga en cuenta que los constructores de datos como Left and Right también son constructores fantasmas:

data Either a b = Left a | Right b

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

La razón es que, aunque el tipo de devolución de estos constructores de datos depende de sus argumentos, aún se generalizan porque solo dependen parcialmente de sus argumentos.

Manera simple de saber si un constructor de datos es un constructor fantasma:

¿Aparecen también todas las variables de tipo que aparecen en el tipo de retorno del constructor de datos en los argumentos del constructor de datos? Si es así, no es un constructor fantasma.

Espero que ayude.

Answer 2

Para la Ratio D3 específicamente, utilizamos tipos ricos como ese para dirigir código dirigido por tipo, por ejemplo, si tiene un campo en algún lugar en tipo Ratio D3 , su editor se envía a un campo de texto que acepta entradas numéricas solamente y muestra una precisión de 3 dígitos . Esto está en contraste, por ejemplo, con newtype Amount = Amount Double donde no mostramos dígitos decimales, pero usamos mil comas y analizamos la entrada como ''10m'' como ''10, 000,000''.

En la representación subyacente, ambos siguen siendo solo Double .

Answer 3

Para responder al "¿cuál es la motivación para usar un tipo fantasma"? Hay dos puntos:

• para hacer que los estados inválidos sean irrepresentables, lo cual está bien explicado en la respuesta de Aadit
• Llevar parte de la información sobre el nivel de tipo

Por ejemplo, puede tener distancias etiquetadas por la unidad de longitud:

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

Y puedes evitar el desastre de Mars Climate Orbiter :

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

Hay ligeras varitions para este "patrón". Puede usar DataKinds para tener un conjunto cerrado de unidades:

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

Y funcionará de manera similar:

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

Pero ahora la Distance puede ser solo en kilómetros o millas, no podemos agregar más unidades más tarde. Eso podría ser útil en algunos casos de uso.

También podríamos hacer:

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

En el caso de distancia, podemos calcular la suma, por ejemplo, traducir a kilómetros si se trata de unidades diferentes. Pero esto no funciona bien para las monedas cuya relación no es constante a lo largo del tiempo, etc.

Y es posible utilizar GADT para eso, lo que puede ser un enfoque más simple en algunas situaciones:

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

Ahora sabemos la unidad también en el nivel de valor:

>>> marathonDistanceInMiles 
MileDistance 26.218749345

Este enfoque simplifica Expr a ejemplo, a partir de la respuesta de 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

Vale la pena señalar que las últimas variaciones requieren extensiones de lenguaje no triviales ( GADTs , DataKinds , KindSignatures ), que pueden no ser compatibles con su compilador. Ese podría ser el caso con el compilador de Mu que Don menciona.