Как добавить аннотацию типа в let binding

Я начинающий (иш) в Haskell, и я нахожу сообщение об ошибке очень трудным для понимания (я думаю, что он приходит со временем). В любом случае, чтобы помочь мне понять мои ошибки, я попытался добавить промежуточную переменную с аннотацией типа в привязке let и обнаружил, что она порождает еще больше ошибок, хотя мой тип (я думаю) правильный.

Пример

f :: a -> a
f x = 
    let x' = x :: a
    in x'

Сгенерировать следующую ошибку

test.hs:3:12:
Couldn't match expected type `a2' with actual type `a'
  `a2' is a rigid type variable bound by
       an expression type signature: a2 at test.hs:3:12
  `a' is a rigid type variable bound by
      the type signature for f :: a -> a at test.hs:1:6
In the expression: x :: a
In an equation for x': x' = x :: a
In the expression: let x' = x :: a in x

Я делаю что-то неправильно или это невозможно сделать?

Ответ 1

Решение

Для этого вам понадобится расширение ScopedTypeVariables, например:

{-# LANGUAGE ScopedTypeVariables #-}

f :: forall a. a -> a
f x = 
    let x' = x :: a
    in x'

Объяснение

Если у вас есть сигнатура типа

f :: a -> a

то это означает, что f является полиморфным и работает для любого выбора a. Таким образом, f может быть используется при типе Int -> Int или при типе Bool -> Bool или при типе [Int -> Bool] -> [Int -> Bool] – что бы вы ни хотели.

Если у вас есть аннотация типа типа

x :: a

это означает аналогичную вещь, а именно, что x следует использовать в любом типе по вашему выбору. Но это не так в вашем случае. Внешняя функция f является полиморфной, но внутри функции x должен быть того же типа a, который пользователь выбрал для внешнего x. По умолчанию Haskell не устанавливает связи между переменными типа, встречающимися в разных типах сигнатур и аннотаций. Однако вы можете сказать это, включив расширение ScopedTypeVariables. Теперь, префикс a -> a с помощью forall a., вы можете явно указать Haskell, чтобы сделать a видимым как переменную определенного типа в определении f. Если вы затем аннотируете x :: a, он ссылается на внешний a, а не на новый полиморфный a.

Ответ 2

Для тех, кто хочет ввести аннотацию привязки вместо выражения - ScopedTypeVariables, вы также можете сделать это!

f1 = do
  let x :: Int = 5
  y :: Int <- someMonadicOperation
  return $ x + y

Ответ 3

Это должно работать:

f :: s -> s
f x =
   let y = undefined :: s
   in  y

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

Update:

Он не работает с полиморфными типами. Но он работает с конкретным типом.

Следующие typechecks:

f :: Int -> Int
f x = let m = x :: Int
      in m

Это приводит к ошибке:

f1 :: a -> a
f1 x = let m = x :: a
       in m