Как я скажу Хаскеллу, что нужно оттаивать?

Question

У меня есть определитель вычислений, который действует на MArray и производит скаляр в той же монаде, здесь я заменил его на return $ fromInteger 1. Так что у меня есть чисто определительная функция, которая использует ее как

det :: (Num e) => Array (Int, Int) e -> e
det a = runST $ (thaw a) >> (return $ fromInteger 1)

И я получаю сообщение об ошибке, что Haskell не может решить, следует ли использовать MArray (STUArray s) Bool (ST s) или кучу других STArray вариантов, и что яЯ должен поставить аннотацию типа, поэтому я делаю

det :: (Num e) => Array (Int, Int) e -> e
det a = runST $ ((thaw a) :: (Num e) => ST s (STArray s (Int, Int) e)) >> (return $ fromInteger 1)

И я получаю

"Couldn't match type 'e1' with 'e'"
"'e1' is a rigid type variable bound by an expression type signature: (Num e1) => ST s1 (STArray s1 (Int, Int) e)"
"'e' is a rigid type variable bound by the type signature for: det :: (Num e) => Array (Int, Int) e -> e"
"Expected type: ST s1 (STArray s1 (Int, Int) e1)"
  "Actual type: ST s1 (STArray s1 (Int, Int) e)"
"In the first argument of '(>>)', namely '((thaw a) :: (Num e) => ST s (STArray s (Int, Int) e))'"

Мне кажется, что не должно быть двух отдельных контекстов для e, потому что thawотличается от fmap, где содержащийся тип может переходить от a до b, для thaw в аргументе и результате содержится тип e.

Плюс, если я укажу e как Double и удалить ограничения Num, затем он прекрасно компилируется.

Наконец, если я удаляю сигнатуру типа для функции, я получаю "Couldn't match expected type 'a0 (Int, Int) e' with actual type 'p' because type variable 'e' would escape its scope", что не имеет никакого смысла, потому что s и e должны быть переменными типа, другого способа записать это не существует.

Итак, как мне заставить Haskell принять экземпляр MArray Я сказал это thaw или выяснитьсамо по себе, что он должен использовать STArray, так как он единственный, который работает дляr general e?

Answer 1

Когда вы делаете

definition :: ... tyvar ...
definition = ... (expr :: ... tyvar ...) ...

Два упоминания tyvar не относятся к одному и тому же. Скорее, у нас есть правило, что все переменные типа во всех явных типах получают forall ed:

definition :: forall tyvar. ... tyvar ...
definition = ... (expr :: forall tyvar. ... tyvar ...) ...

То есть переменные типа не имеют области видимости. Когда вы написали

thaw a :: ST s (STArray s (Int, Int) e) -- this is the "more correct" version of what you wrote

, вы на самом деле написали

thaw a :: forall e. ST s (STArray s (Int, Int) e) 

Таким образом, вы сказали: «Возьмите Array типа элемента e и преобразуйте его в STArray каждого элемента. тип". Это не работает.

Решение для Haskell 98 состоит в том, чтобы снова использовать вспомогательную функцию для связывания типа e:

thawST :: Array i e -> ST s (STArray s i e)
thawST x = thaw x

det a = runST $ thawST a >> return 1

Конечно, thawST - это просто thawс ограниченной подписью, так что это также работает (это решение несколько менее общее):

det a = runST $ (thaw :: Array i e -> ST s (STArray s i e)) a >> return 1

Если вы согласны с языковыми расширениями, вы можете использовать ExplicitForAll и ScopedTypeVariables:

det :: forall e. Num e => Array (Int, Int) e -> e -- e will be bound in the definition
det a = runST $ (thaw a :: ST s (STArray s (Int, Int) e)) >> return 1
-- s is not in scope, gets implicitly foralled
-- e is in scope, refers to that variable

Или вы можете использовать TypeApplications вместо подписи

thaw :: (Ix i, IArray a e, MArray b e m) => a i e -> m (b i e)
-- so it takes type arguments in the order i(ndex) a(rray) e(lement) b(rray) m(onad)

det :: forall e. Num e => Array (Int, Int) e -> e
det a = runST $ thaw @_ @_ @_ @(STArray _) a >> return 1
-- _ means "infer this"
-- so we left the i, a, e, and m types to be inferred
-- and we specified that the result array was an STArray and left the state type inferred
-- the state type is currently unnamed: it's given to us by runST
-- but you need another type signature (runST (_ :: forall s. ST s <result>))
-- to actually reference it by name
-- therefore, we are forced to use _ and let it be inferred in the argument to thaw