Типы «сопоставления с образцом» в Haskell

Я хочу функцию f что действует как приращение Ints и как тождество для всех остальных типов. Я попытался включить TypeApplications extension и сделайте это наиболее простым способом:

      f :: forall a. a -> a
f @Int x = x + 1
f @_   x = x

Но расширение не поддерживает такие шаблоны:

      <interactive>:6:1: error: Parse error in pattern: f @Int

Есть ли в Haskell сопоставление с образцом для типов (или аналогичный механизм)?

Источник

3 ответа

Решение

Как уже говорилось, этого невозможно достичь в Haskell, поскольку это нарушило бы одно из фундаментальных свойств параметрического полиморфизма, известное как «параметричность», которое гарантирует, что любая полиморфная функция удовлетворяет определенному свойству, известному как «теорема свободы».

В частности, завершающая функция типа forall a. a -> aдолжна быть личность. Других возможных реализаций нет.

При этом, если мы допустим ограничение на тип a, это становится возможным. Обычно тестирование типов во время выполнения выполняется в Haskell через Typeable тип класс:

      f :: forall a. Typeable a => a -> a
f x = case eqT @a @Int of    -- Is a ~ Int ?
   Just Refl -> x + 1        -- If it is, we can add one.
   Nothing   -> x            -- Otherwise, return x as-is.

Для этого требуется набор расширений GHC, а для импорта Data.Typeable.

Источник

Есть, но у вас не может быть модели провала, как на уровне вычислений. То есть на уровне вычислений я мог бы написать

      f 0 = 42
f n = n-1

с рисунком провала nэто работает точно, когда ни один из других шаблонов не совпал. На уровне типов вы не можете этого сделать - даже вложенные в другие шаблоны. У вас может быть шаблон, который соответствует чему угодно, но не "ничему другому" - если вы сопоставите что-либо, у вас не может быть никаких других шаблонов.

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

      class F a where f :: a -> a
instance F Int where f = succ
instance F Bool where f = id
instance F [a] where f = id

Последнее показывает пример того, что я имел в виду раньше, где у вас может быть шаблон, который соответствует чему угодно, но не шаблон, который соответствует "чему-либо еще": [a] прекрасный пример, но он исключает создание [Bool] экземпляр позже.

Источник

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

      {-# Language
    AllowAmbiguousTypes,
    FlexibleInstances,
    TypeFamilies #-}

-- The class of overloads of ‘f’.
class F a where
  type family T a   -- Or: ‘type T a’
  f :: T a -> T a

-- The “default” catch-all overload.
instance {-# Overlappable #-} F a where
  type instance T a = a  -- Or: ‘type T a = a’
  f x = x

-- More specific instance, selected when ‘a ~ Int’.
instance {-# Overlapping #-} F Int where
  type instance T Int = Int
  f x = x + 1

потом f @Int 1 дает 2, а также f 'c' дает 'c'.

Но в этом случае семейство типов не нужно, потому что оно является тождеством - я включаю его в целях обобщения. Если вы хотите создавать типы путем сопоставления с образцом для типов, как функция, то семейство закрытых типов отлично подходит:

      {-# Language
    KindSignatures,
    TypeFamilies #-}

import Data.Int
import Data.Word
import Data.Kind (Type)

type family Unsigned (a :: Type) :: Type where
  Unsigned Int   = Word
  Unsigned Int8  = Word8
  Unsigned Int16 = Word16
  Unsigned Int32 = Word32
  Unsigned Int64 = Word64
  Unsigned a     = a

Возвращаясь к вашему вопросу, вот оригинальный пример с простыми классами типов:

      class F a where
  f :: a -> a

instance {-# Overlappable #-} F a where
  f x = x

instance {-# Overlapping #-} F Int where
  f x = x + 1

К сожалению, нет понятия «закрытый класс типов», который позволил бы избежать перекрытия экземпляров. В этом случае это довольно легко, но проблемы с согласованностью могут возникнуть в более сложных случаях, особенно с MultiParamTypeClasses. В общем когда это возможно , предпочтительнее случае,добавлять новый метод вместо написания перекрывающихся экземпляров .

Обратите внимание, что в любом случае f теперь есть F a ограничение, например, последнее (F a) => a -> a. Вы не можете избежать некоторых изменений типа; в Haskell полиморфизм означает параметрический полиморфизм, чтобы сохранить свойство, которое позволяет стирать типы во время компиляции.

Другие варианты включают GADT:

      data FArg a where
  FInt :: Int -> FArg Int
  FAny :: a -> FArg a

f :: FArg a -> a
f (FInt x) = x + 1  -- Here we have ‘a ~ Int’ in scope.
f (FAny x) = x

Или (уже упоминалось в других ответах) a Typeable ограничение для динамической типизации:

      {-# Language
    BlockArguments,
    ScopedTypeVariables #-}

import Data.Typeable (Typeable, eqT)
import Data.Type.Equality ((:~:)(Refl))

f :: forall a. (Typeable a) => a -> a
f x = fromMaybe x do
  Refl <- eqT @a @Int
  pure (x + 1)
Источник
Другие вопросы по тегам