Характеризуя тип функций, которые могут принимать `()` в качестве входных данных (без мономорфизации)

Question

Вот несколько простых функций:

      f1 :: () -> ()
f1 () = ()

f2 :: a -> a
f2 a = a

f3 :: a -> (a, a)
f3 a = (a, a)

f4 :: (a, b) -> a
f4 (a, b) = a

Все, и могут принимать в качестве входных данных. С другой стороны, конечно, f4 не могу принять; f4 () это ошибка типа.

Можно ли теоретически охарактеризовать то, что f1, f2, и f3есть общее? В частности, можно ли определить acceptsUnit функция, такая, что acceptsUnit f1, acceptsUnit f2, и acceptsUnit f3 хорошо напечатаны, но acceptsUnit f4 это ошибка типа - и не имеющая другого эффекта?

Следующее выполняет часть работы, но мономорфизирует его ввод (в Haskell, и я собираю в Hindley-Milner) и, следовательно, имеет эффект, помимо простого утверждения, что его ввод может принимать ():

      acceptsUnit :: (() -> a) -> (() -> a)
acceptsUnit = id

-- acceptsUnit f4     ~> error 😊
-- acceptsUnit f3 'a' ~> error ☹️

Такая же мономорфизация, конечно, происходит и в следующем. В этом случае аннотированный тип acceptsUnit' это его основной тип.

      acceptsUnit' :: (() -> a) -> (() -> a)
acceptsUnit' f = let x = f () in f

Answer 1

Теоретически типографически охарактеризовать то, что f1, f2, и f3 но нет f4есть общее. На языке Хиндли-Милнера первые три имеют политипы, которые могут быть специализированы до политипа формы:

      forall a1...an. () -> tau

для n> = 0 и tau произвольный монотип. Четвертый не может.

Можете ли вы написать функцию, которая принимает первые три в качестве аргумента, но отклоняет четвертый? Что ж, это зависит от системы типов, которую вы используете, и от той широты, которая у вас есть для структурирования вашей функции. В обычной системе типов Хиндли-Милнера и / или стандартной системе типов Haskell, если у вас есть возможность передать две копии вашей функции-кандидата в функцию принятия, будет работать следующее:

      acceptsUnit :: (() -> a) -> (b -> c) -> (b -> c)
acceptsUnit = flip const

f1 :: () -> ()
f1 () = ()

f2 :: a -> a
f2 a = a

f3 :: a -> (a, a)
f3 a = (a, a)

f4 :: (a, b) -> a
f4 (a, b) = a

main = do
  print $ acceptsUnit f1 f1 ()
  print $ acceptsUnit f2 f2 10
  print $ acceptsUnit f3 f3 10
  -- print $ acceptsUnit f4 f4  -- type error

Вероятно, это лучшее, что вы можете сделать со стандартным Haskell (и, вероятно, лучшее, что вы можете сделать с расширениями системы типов Haskell плюс GHC, иначе кто-то уже что-то нашел бы).

Если вы можете определить свою собственную систему набора текста с ее собственными правилами набора текста, то пределом нет.