Найти соответствие параметрическому параметру - PullRequest
Новая
       17

Найти соответствие параметрическому параметру

5 голосов
/ 27 марта 2019

Можно ли сопоставить параметр типа для произвольного типа через семейства типов или иным образом?

Я пытаюсь написать функцию типа 

type family Match s t a

, которая принимает две структуры, s и t (которые предполагают две разные параметризации одного и того же типа, например Maybe Int и Maybe String) и параметр, с которым будет сопоставляться.Если соответствующий параметр найден, функция type предоставляет замену.В противном случае он предоставляет исходный параметр.

Match (Maybe a) (Maybe b) a ~ b
Match (Maybe a) (Maybe b) c ~ c

Моя попытка реализации: 

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}

import Data.Type.Equality
import Data.Type.Bool

type family Match (s::k) (t::k) (a :: * ) :: * where
  Match (f a :: *) (g b :: *) c = If ((a == c)) b c

Очевидно, семейство работает, как и планировалось, когда найден параметр: 

>  :t (undefined :: (Match (Maybe a) (Maybe b) a))
(undefined :: (Match (Maybe a) (Maybe b) a)) :: b

Но не для случаев, когда не совпадают:

 >  :t (undefined :: (Match (Maybe a) (Maybe b) c))
     Couldn't match type ‘If
                             ghc-prim-0.5.0.0:GHC.Types.*
                             (Data.Type.Equality.EqStar a0 c0)
                             b0
                             c0’
                     with ‘If
                             ghc-prim-0.5.0.0:GHC.Types.*   (Data.Type.Equality.EqStar a c) b c’
      Expected type: Match * (Maybe a) (Maybe b) c
        Actual type: Match * (Maybe a0) (Maybe b0) c0
      NB: ‘If’ is a type function, and may not be injective
      The type variables ‘a0’, ‘b0’, ‘c0’ are ambiguous
    • In the ambiguity check for an expression type signature
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In an expression type signature: Match (Maybe a) (Maybe b) c
      In the expression: (undefined :: Match (Maybe a) (Maybe b) c)

Возможно ли то, что я спрашиваю, возможно?Это не должно быть семейства типов, я открыт для других подходов.Ото, поможет ли здесь использование неоднозначных типов?Я не знаю подводных камней, поэтому я колеблюсь.

Спасибо!

1 Ответ

3 голосов
/ 28 марта 2019

Вы просите о двух разных вещах. Вы искали

[функция типа], которая принимает две структуры: s и t (которые предполагают две разные параметризации одного и того же типа, например Maybe Int и Maybe String) и параметр, который будет сопоставляться против. Если соответствующий параметр найден, функция type предоставляет замену. В противном случае он предоставляет исходный параметр.

Вы уже в основном написали это. Вам, вероятно, следует избегать использования (==), потому что вам разрешено использовать нелинейное сопоставление, которое обычно лучше: 

type family Match (a :: i) (b :: i) (c :: o) :: o where
    Match (f a) (f b) a = b
    Match (f a) (f b) b = a
    Match _     _     c = c

Позже вы определяете две функции и хотите, чтобы обе компилировались. 

undefined :: Match (Maybe a) (Maybe b) a
undefined :: Match (Maybe a) (Maybe b) c

Первый принимает два типа в качестве аргументов: 

\@(a :: Type) @(b :: Type) -> (undefined :: Match (Maybe a) (Maybe b) a)

Сигнатура типа соответствует первому уравнению Match и уменьшается до a. 

\@(a :: Type) @(b :: Type) -> (undefined :: a)

, который позволяет выводить правильные параметры для функции undefined: 

\@a @(b :: Type) -> undefined @'GHC.Types.LiftedRep @a

Вторая функция 

\@(a :: Type) @(b :: Type) @(c :: Type) -> (undefined :: Match (Maybe a) (Maybe b) c)

Было бы неправильно выводить аргумент undefined как приложение семейства типов Match (Maybe a) (Maybe b) c. Есть много вопросов об ошибках «неоднозначного типа», в которых указана причина. Скорее, приложение семейства типов должно быть сокращено. Но это не может уменьшить. Он соответствует третьему уравнению, но также может соответствовать первому и второму уравнениям, если a ~ c или b ~ c, поэтому было бы неправильно переходить к запасному варианту, когда основное еще доступно. Вы можете спросить: «Почему a / b и c не отличаются?» Ответ в том, что a, b и c - это просто переменные (которые являются переменными типа) и просто имена для значений (которые являются типами). Эти значения приведены в качестве аргументов вашей функции. Если бы я дал вам x, y :: Int и попросил бы указать значение if x == y then "Yes" else "No", вы бы не смогли мне сказать, потому что вы не знаете значений x и y. Тем не менее, вы спросили Хаскелла: «Вот, a, b, c :: Type. Что такое if a == c then b else if b == c then a else c?». Это так же неопровержимо. Невозможно отличить переменные с одинаковыми значениями, потому что это действительно подорвало бы основы Haskell.

Обратите внимание, что есть довольно дерзкий ответ на вопрос, который я вам дал. Вы можете просто сказать «значение if x == y then "Yes" else "No" равно if x == y then "Yes" else "No"». Аналогично, я могу войти и вручную предоставить аргумент типа приложения семейства невосстановленных типов в undefined, чтобы определить вашу функцию, разрешив неоднозначные типы. Больше нет необходимости выводить аргумент undefined, пытаясь (и не получая) уменьшить приложение Match. 

fun :: forall a b c. Match (Maybe a) (Maybe b) c
fun = undefined @_ @(Match (Maybe a) (Maybe b) c)

Это аккуратно обходит невозможный вопрос. Тип результата fun теперь откладывается до момента его использования, то есть сила / проклятие AllowAmbiguousTypes. Теперь fun @Int @String @Int :: String по первому уравнению, fun @Int @String @String :: Int по второму уравнению и fun @Int @String @Bool :: Bool по третьему уравнению. Невозможно заставить эту функцию «выбрать» третье уравнение в определении.

...