Совпадение образцов по типу ранга 2

Ответ 1

Я думаю, что наличие грубой ментальной модели водопровода на уровне типа, которое здесь играет, очень важно, поэтому я собираюсь поговорить о "неявных вещах" немного подробнее и тщательно проанализировать вашу проблему только после этого. Читатели, заинтересованные только в прямом решении вопроса, могут перейти к подразделу "Согласование шаблонов по полиморфным значениям" и концу.

1. Неявные аргументы функции

Аргументы типа

GHC компилирует Haskell на небольшой промежуточный язык под названием Core, который по существу представляет собой ранговое полиморфное типизированное лямбда-исчисление, называемое System F (плюс некоторые расширения). Ниже я буду использовать Haskell рядом с примечанием, несколько напоминающим Core; Надеюсь, это не слишком запутанно.

В Core, полиморфные функции - это функции, которые принимают типы в качестве дополнительных аргументов, а аргументы в дальнейшем могут ссылаться на эти типы или иметь эти типы:

-- in Haskell
const :: forall (a :: *) (b :: *). a -> b -> a
const x y = x

-- in pseudo-Core
const' :: (a :: *) -> (b :: *) -> a -> b -> a
const' a b x y = x 

Это означает, что мы должны также предоставлять аргументы типа этим функциям всякий раз, когда мы хотим их использовать. В выводе типа Haskell обычно вычисляются аргументы типа и поставляет их автоматически, но если мы посмотрим на вывод Core (например, см. Этот введение, как это сделать), аргументы типа и приложения видны повсюду. Построение ментальной модели этого упрощает определение кода более высокого ранга:

-- Haskell
poly :: (forall a. a -> a) -> b -> (Int, b)
poly f x = (f 0, f x)

-- pseudo-Core
poly' :: (b :: *) -> ((a :: *) -> a -> a) -> b -> (Int, b)
poly' b f x = (f Int 0, f b x)

И понятно, почему некоторые вещи не проверяются typecheck:

wrong :: (a -> a) -> (Int, Bool)
wrong f = (f 0, f True)

wrong' :: (a :: *) -> (a -> a) -> (Int, Bool)
wrong' a f = (f ?, f ?) -- f takes an "a", not Int or Bool. 

Аргументы ограничения класса

-- Haskell
show :: forall a. Show a => a -> String
show x = show x

-- pseudo-Core
show' :: (a :: *) -> Show a -> a -> String
show' a (ShowDict showa) x = showa x 

Что такое ShowDict и Show a здесь? ShowDict - это всего лишь запись Haskell, содержащая экземпляр show, и GHC генерирует такие записи для каждого экземпляра класса. Show a - это только тип записи этого экземпляра:

-- We translate classes to a record type:
class Show a where show :: a -> string

data Show a = ShowDict (show :: a -> String)

-- And translate instances to concrete records of the class type:
instance Show () where show () = "()"

showUnit :: Show ()
showUnit = ShowDict (\() -> "()")

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

data Foo = Foo

-- instance Show Foo where show _ = "Foo"
showFoo :: Show Foo
showFoo = ShowDict (\_ -> "Foo")

-- The compiler fills in an instance from top level
fooStr :: String
fooStr = show' Foo showFoo Foo 

polyShow :: (Show a, Show b) => a -> b -> String
polyShow a b = show a ++ show b

-- Here we get the instances as arguments (also, note how (++) also takes an extra
-- type argument, since (++) :: forall a. [a] -> [a] -> [a])
polyShow' :: (a :: *) -> (b :: *) -> Show a -> Show b -> a -> b -> String
polyShow' a b (ShowDict showa) (ShowDict showb) a b -> (++) Char (showa a) (showb b) 

Совпадение шаблонов по полиморфным значениям

В Haskell сопоставление шаблонов по функциям не имеет смысла. Полиморфные значения также можно рассматривать как функции, но мы можем сопоставить их с образцом, как в ошибочном примере OP runfun1. Тем не менее, все неявные аргументы должны быть выведены в область видимости, иначе простой акт сопоставления шаблонов является ошибкой типа:

import Data.Monoid

-- it a type error even if we don't use "a" or "n".
-- foo :: (forall a. Monoid a => (a, Int)) -> Int
-- foo (a, n) = 0 

foo :: ((a :: *) -> Monoid a -> (a, Int)) -> Int
foo f = ? -- What are we going to apply f to?

Другими словами, при сопоставлении шаблонов на полиморфном значении мы утверждаем, что все неявные аргументы уже применяются. В случае foo здесь, хотя в приложении Haskell нет синтаксиса для приложения типа, мы можем посыпать аннотации типов:

{-# LANGUAGE ScopedTypeVariables, RankNTypes #-}

foo :: (forall a. Monoid a => (a, Int)) -> Int
foo x = case (x :: (String, Int)) of (_, n) -> n

-- or alternatively
foo ((_ :: String), n) = n 

Опять же, псевдо-ядро делает ситуацию более ясной:

foo :: ((a :: *) -> Monoid a -> (a, Int)) -> Int
foo f = case f String monoidString of (_ , n) -> n 

Здесь monoidString - это некоторый доступный Monoid экземпляр String.

2. Неявные поля данных

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

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

Стандартный пример:

{-# LANGUAGE GADTs #-}

data Showy where
    Showy :: forall a. Show a => a -> Showy

-- pseudo-Core
data Showy where
    Showy :: (a :: *) -> Show a -> a -> Showy

-- when constructing "Showy", "Show a" must be also available:
someShowy :: Showy
someShowy = Showy (300 :: Int)

-- in pseudo-Core
someShowy' = Showy Int showInt 300 

-- When pattern matching on "Showy", we get an instance in scope too
showShowy :: Showy -> String
showShowy (Showy x) = show x 

showShowy' :: Showy -> String
showShowy' (Showy a showa x) = showa x

3. Взглянув на пример OP

Мы имеем функцию

runFun1 :: (Vector v r, MVector (Mutable v) r) => 
  (forall m . (PrimMonad m) => DimFun (Mutable v) m r) -> v r -> v r
runFun1 [email protected](DimFun dim t) x | V.length x == dim = runST $ do
    y <- thaw x
    t y
    unsafeFreeze y

Помните, что сопоставление шаблонов по полиморфным значениям утверждает, что все неявные аргументы доступны в области. Кроме того, здесь, в точке сопоставления шаблонов, в области не существует m, не говоря уже о экземпляре PrimMonad.

С GHC 7.8.x рекомендуется использовать типы отверстий:

runFun1 :: (Vector v r, MVector (Mutable v) r) => 
  (forall m . (PrimMonad m) => DimFun (Mutable v) m r) -> v r -> v r
runFun1 (DimFun dim t) x | V.length x == dim = _

Теперь GHC должным образом отобразит тип отверстия, а также типы переменных в контексте. Мы можем видеть, что t имеет тип Mutable v (PrimState m0) r -> m0 (), и мы также видим, что m0 нигде не упоминается как связанный. Действительно, это печально известная "двусмысленная" переменная типа, созданная GHC в качестве заполнителя.

Итак, почему мы не пытаемся вручную предоставить аргументы, как в предыдущем примере с экземпляром Monoid? Мы знаем, что мы будем использовать t внутри действия ST, поэтому мы можем попробовать установить m как ST s, а GHC автоматически применит для нас экземпляр PrimMonad:

runFun1 :: forall v r. (Vector v r, MVector (Mutable v) r) => 
  (forall m . (PrimMonad m) => DimFun (Mutable v) m r) -> v r -> v r
runFun1 (DimFun dim (t :: Mutable v s r -> ST s ())) x 
    | V.length x == dim = runST $ do 
        y <- thaw x
        t y
        unsafeFreeze y

... за исключением того, что он не работает, и мы получаем ошибку "Couldn't match type ‘s’ with ‘s1’ because type variable ‘s1’ would escape its scope".

Оказывается - неудивительно, что мы забыли о еще одном неявном аргументе. Напомним тип runST:

runST :: (forall s. ST s a) -> a

Мы можем представить себе, что runST принимает функцию типа ((s :: PrimState ST) -> ST s a), а затем наш код выглядит следующим образом:

runST $ \s -> do
    y <- thaw x   -- y :: Mutable v s r
    t y           -- error: "t" takes a "Mutable v s r" with a different "s". 
    unsafeFreeze y 

Тип аргумента s in t беззвучно вводится в самой внешней области:

runFun1 :: forall v s r. ...

И, таким образом, два s -es различны.

Возможным решением является сопоставление шаблонов в аргументе DimFun внутри действия ST. Там правильный s находится в области видимости, и GHC может поставлять ST s как m:

runFun1 :: forall v r. (Vector v r, MVector (Mutable v) r) => 
    (forall m . PrimMonad m => DimFun (Mutable v) m r) -> v r -> v r
runFun1 dimfun x = runST $ do
    y <- thaw x
    case dimfun of
        DimFun dim t | dim == M.length y -> t y
    unsafeFreeze y

С некоторыми определенными параметрами:

runST $ \s -> do
    y <- thaw x
    case dimfun (ST s) primMonadST of
         DimFun dim t | dim == M.length y -> t y
    unsafeFreeze y 

Как упражнение, позвольте преобразовать всю функцию в псевдо-ядро (но не отменяем синтаксис do, потому что это будет слишком уродливо):

-- the full types of the functions involved, for reference
thaw :: forall m v a. (PrimMonad m, V.Vector v a) => v a -> m (V.Mutable v (PrimState m) a)
runST :: forall a. (forall s. ST s a) -> a
unsafeFreeze :: forall m v a. (PrimMonad m, Vector v a) => Mutable v (PrimState m) a -> v a 
M.length :: forall v s a. MVector v s a -> Int
(==) :: forall a. Eq a => a -> a -> Bool

runFun1 :: 
    (v :: * -> *) -> (r :: *) 
    -> Vector v r -> MVector (Mutable v) r
    -> ((m :: (* -> *)) -> PrimMonad m -> DimFun (Mutable v) m r)
    -> v r -> v r
runFun1 v r vecInstance mvecInstance dimfun x = runST r $ \s -> do
    y <- thaw (ST s) v r primMonadST vecInstance x
    case dimFun (ST s) primMonadST of
        DimFun dim t | (==) Int eqInt dim (M.length v s r y) -> t y
    unsafeFreeze (ST s) v r primMonadST vecInstance y

Это был глоток.

Теперь мы хорошо подготовлены, чтобы объяснить, почему runFun2 работал:

runFun2 :: (Vector v r, MVector (Mutable v) r) => 
  (forall m . (PrimMonad m) => DimFun (Mutable v) m r) -> v r -> v r
runFun2 t x = runST $ do
  y <- thaw x
  evalFun t y
  unsafeFreeze y

evalFun :: (PrimMonad m, MVector v r) => DimFun v m r -> v (PrimState m) r -> m ()
evalFun (DimFun dim f) y | dim == M.length y = f y

evalFun - это просто полиморфная функция, которая вызывается в нужном месте (мы в конечном итоге сопоставляем соответствие шаблону на t в нужном месте), где правильный ST s доступен как аргумент m.

Как система типов становится более сложной, сопоставление образцов становится все более серьезным делом, с далеко идущими последствиями и нетривиальными требованиями. В конце спектра вы найдете полноразмерные языки и вспомогательные документы, такие как Agda, Idris или Coq, где сопоставление образцов на части данных может означать принятие произвольного логического предложения как истинного в определенной ветки вашей программы.

Ответ 2

Хотя @AndrasKovacs дал отличный ответ, я думаю, стоит отметить, как вообще избежать этой гадости. Этот ответ на связанный с вами вопрос показывает, как "правильное" определение для DimFun заставляет все вещи ранга-2 уйти.

Определив DimFun как

data DimFun v r = 
  DimFun {dim::Int, func :: forall s . (PrimMonad s) => v (PrimState s) r -> s ()}

runFun1 становится:

runFun1 :: (Vector v r)
        => DimFun (Mutable v) r -> v r -> v r
runFun1 (DimFun dim t) x | dim == V.length x = runST $ do
  y <- thaw x
  t y
  unsafeFreeze y

и компилируется без проблем.

Ответ 3

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

То есть я не думаю, что GHC может унифицировать тип значения, соответствующего шаблону (DimFun dim t), с типом (forall m . (PrimMonad m) => DimFun (Mutable v) m r).

Обратите внимание, что совпадение шаблона в evalFun выглядит аналогично, но разрешено помещать ограничения на m, так как квантификация ограничена всем evalFun; в constrast, runFun1 как меньшая область для количественной оценки m.

НТН