haskell - ConstraintKinds explicado en un ejemplo super simple

ghc type-kinds

Question

¿Qué es una clase de restricción ?

¿Por qué alguien lo usaría (en la práctica)?

¿Para que sirve?

¿Podría dar un ejemplo de código simple para ilustrar las respuestas a las dos preguntas anteriores?

¿Por qué se utiliza en this código, por ejemplo?

Answer 1

Bueno, voy a mencionar dos cosas prácticas que te permite hacer:

1. Parametrizar un tipo por una restricción de clase de tipo
2. Escriba clases de tipo que permitan a sus instancias especificar las restricciones que necesitan.

Quizás sea mejor ilustrar esto con un ejemplo. Una de las verrugas clásicas de Haskell es que no puede crear una instancia de Functor para tipos que impongan una restricción de clase en su parámetro de tipo; por ejemplo, la clase Set en la biblioteca de containers , que requiere una restricción Ord en sus elementos. La razón es que en Haskell "vanilla", tendrías que tener la restricción en la propia clase:

class OrdFunctor f where
    fmap :: Ord b => (a -> b) -> f a -> f b

... pero entonces esta clase solo funciona para tipos que requieren específicamente una restricción Ord . ¡No es una solución general!

Entonces, ¿qué pasaría si pudiéramos eliminar esa definición de clase y abstraer la restricción Ord , permitiendo que las instancias individuales digan qué restricción requieren? Bueno, ConstraintKinds plus TypeFamilies permite que:

{-# LANGUAGE ConstraintKinds, TypeFamilies, FlexibleInstances #-}

import Prelude hiding (Functor(..))
import GHC.Exts (Constraint)
import Data.Set (Set)
import qualified Data.Set as Set

-- | A ''Functor'' over types that satisfy some constraint.
class Functor f where
   -- | The constraint on the allowed element types.  Each
   -- instance gets to choose for itself what this is.
   type Allowed f :: * -> Constraint

   fmap :: Allowed f b => (a -> b) -> f a -> f b

instance Functor Set where
    -- | ''Set'' gets to pick ''Ord'' as the constraint.
    type Allowed Set = Ord
    fmap = Set.map

instance Functor [] where
    -- | And `[]` can pick a different constraint than `Set` does.
    type Allowed [] = NoConstraint
    fmap = map

-- | A dummy class that means "no constraint."
class NoConstraint a where

-- | All types are trivially instances of ''NoConstraint''.
instance NoConstraint a where

(Tenga en cuenta que este no es el único obstáculo para crear una instancia de Functor para Set ; consulte esta discusión . También, NoConstraint esta respuesta por el truco de NoConstraint ).

Sin embargo, este tipo de solución todavía no se ha adoptado en general, porque ConstraintKinds es todavía una característica más o menos nueva.

Otro uso de ConstraintKinds es parametrizar un tipo por una restricción de clase o clase. Reproduciré este código de "Ejemplo de forma" de Haskell que escribí :

{-# LANGUAGE GADTs, ConstraintKinds, KindSignatures, DeriveDataTypeable #-}
{-# LANGUAGE TypeOperators, ScopedTypeVariables, FlexibleInstances #-}

module Shape where

import Control.Applicative ((<$>), (<|>))
import Data.Maybe (mapMaybe)
import Data.Typeable
import GHC.Exts (Constraint)

-- | Generic, reflective, heterogeneous container for instances
-- of a type class.
data Object (constraint :: * -> Constraint) where
    Obj :: (Typeable a, constraint a) => a -> Object constraint
           deriving Typeable

-- | Downcast an ''Object'' to any type that satisfies the relevant
-- constraints.
downcast :: forall a constraint. (Typeable a, constraint a) =>
            Object constraint -> Maybe a
downcast (Obj (value :: b)) = 
  case eqT :: Maybe (a :~: b) of
    Just Refl -> Just value
    Nothing -> Nothing

Aquí el parámetro del tipo de Object es una clase de tipo (clase * -> Constraint ), por lo que puede tener tipos como Object Shape donde Shape es una clase:

class Shape shape where
  getArea :: shape -> Double

-- Note how the ''Object'' type is parametrized by ''Shape'', a class 
-- constraint.  That''s the sort of thing ConstraintKinds enables.
instance Shape (Object Shape) where
    getArea (Obj o) = getArea o

Lo que hace el tipo de Object es una combinación de dos características:

1. Un tipo existencial (habilitado aquí por GADTs ), que nos permite almacenar valores de tipos heterogéneos dentro del mismo tipo de Object .
2. ConstraintKinds , que nos permite, en lugar de codificar el Object a un conjunto específico de restricciones de clase, hacer que los usuarios del tipo de Object especifiquen la restricción que desean como parámetro para el tipo de Object .

Y ahora con eso no solo podemos hacer una lista heterogénea de instancias de Shape :

data Circle = Circle { radius :: Double }
            deriving Typeable

instance Shape Circle where
  getArea (Circle radius) = pi * radius^2


data Rectangle = Rectangle { height :: Double, width :: Double }
               deriving Typeable

instance Shape Rectangle where
  getArea (Rectangle height width) = height * width

exampleData :: [Object Shape]
exampleData = [Obj (Circle 1.5), Obj (Rectangle 2 3)]

... pero gracias a la restricción Typeable en Object , podemos reducirla : si Typeable correctamente el tipo contenido dentro de un Object , podemos recuperar ese tipo original:

-- | For each ''Shape'' in the list, try to cast it to a Circle.  If we
-- succeed, then pass the result to a monomorphic function that 
-- demands a ''Circle''.  Evaluates to:
--
-- >>> example
-- ["A Circle of radius 1.5","A Shape with area 6.0"]
example :: [String]
example = mapMaybe step exampleData
  where step shape = describeCircle <$> (downcast shape)
                 <|> Just (describeShape shape)

describeCircle :: Circle -> String
describeCircle (Circle radius) = "A Circle of radius " ++ show radius

describeShape :: Shape a => a -> String
describeShape shape = "A Shape with area " ++ show (getArea shape)

Answer 2

La extensión ConstraintKind permite el uso del tipo Constraint . Cada expresión que aparece en un contexto (generalmente las cosas entre :: y => ), tiene una Constraint tipo. Por ejemplo, en ghci:

Prelude> :kind Num
Num :: * -> Constraint

En general, no es posible usar este tipo manualmente, pero la extensión ConstraintKinds permite. Por ejemplo, ahora se puede escribir:

Prelude> :set -XConstraintKinds
Prelude> type HasRequiredProperties a = (Num a, Read a, Show a, Monoid a)
Prelude> :kind HasRequiredProperties
HasRequiredProperties :: * -> Constraint

Ahora que tiene algo que toma un tipo (tipo * ) y da una Constraint , puede escribir código como este.

Prelude> :{
Prelude| let myAwesomeFunction :: HasRequiredProperties a => a -> IO ()
Prelude|     myAwesomeFunction x = undefined
Prelude| :}

Es posible que la biblioteca a la que se vincula use MonadWidget como un sinónimo de tipo con Constraint , pero tendrá que mirar más de cerca para asegurarse.