ConstraintKinds объяснил на супер простом примере

Что такое тип ограничения?

Зачем кому-то использовать это (на практике)?

Для чего это?

Не могли бы вы привести простой пример кода, чтобы проиллюстрировать ответы на два предыдущих вопроса?

Почему это используется в этом коде, например?

2 ответа

Решение

Хорошо, я упомяну две практические вещи, которые это позволяет вам сделать:

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

Может быть, лучше проиллюстрировать это на примере. Одна из классических бородавок Хаскелла в том, что вы не можете сделать Functor экземпляр для типов, которые налагают ограничение класса на их параметр типа; например, Set класс в containers библиотека, которая требует Ord ограничение на его элементы. Причина в том, что в "ванильном" Хаскеле вам нужно будет ограничить сам класс:

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

... но тогда этот класс работает только для типов, которые требуют специально Ord ограничение. Не общее решение!

Так что, если бы мы могли взять это определение класса и абстрагироваться от Ord ограничение, позволяющее отдельным экземплярам сказать, какое ограничение им требуется? Что ж, ConstraintKinds плюс TypeFamilies разрешить это:

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

(Обратите внимание, что это не единственное препятствие для создания Functor экземпляр для Set; увидеть это обсуждение. Кроме того, кредит на этот ответ для NoConstraint хитрость.)

Такого рода решение еще не было принято вообще, хотя, потому что ConstraintKinds все еще более или менее новая функция.


Другое использование ConstraintKinds заключается в параметризации типа с помощью ограничения класса или класса. Я воспроизведу этот код "Образца формы" на Haskell, который я написал:

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

Здесь параметр Object тип является типом класса (вид * -> Constraint), так что вы можете иметь такие типы, как Object Shape где Shape это класс:

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

Что за Object Тип делает это сочетание двух функций:

  1. Экзистенциальный тип (включается здесь GADTs), что позволяет хранить значения разнородных типов внутри одного Object тип.
  2. ConstraintKinds, что позволяет нам, вместо жесткого кодирования Object к некоторому определенному набору ограничений класса, пользователи Object Тип укажите ограничение, которое они хотят в качестве параметра для Object тип.

И теперь с этим мы можем не только составить разнородный список 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)]

... но благодаря Typeable ограничение в Object мы можем опустить вниз: если мы правильно угадать тип, содержащийся в Object мы можем восстановить этот оригинальный тип:

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

ConstraintKind расширение позволяет использовать Constraint Добрый. Каждое выражение, которое появляется в контексте (как правило, между :: а также =>), имеет вид Constraint, Например, в ghci:

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

Как правило, невозможно использовать этот вид вручную, но ConstraintKinds расширение позволяет это. Например, теперь можно написать:

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

Теперь, когда у вас есть что-то, что принимает тип (вид *) и дает ConstraintВы можете написать код, как это.

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

Возможно, библиотека, на которую вы ссылаетесь, использует MonadWidget как синоним типа с Constraint добрый, но вам придется внимательно посмотреть, чтобы убедиться.

Другие вопросы по тегам