Ответ 1
Параметричность - это значения типов с переменными. T
не имеет переменных, поэтому параметричность не применяется. Infact, T имеет много жителей.
ap :: T -> T -> T
ap (MkT f) t = f t
idT :: T
idT = MkT id
constT :: T
constT = MkT $ \t -> MkT $ \_ -> t
axiom_sT :: T
axiom_sT = MkT $ \f -> MkT $ \g -> MkT $ \a -> (g `ap` a) `ap` (f `ap` a)
Тип T
представляет собой реализацию Untyped Lambda Calculus, универсальной формальной системы, эквивалентной по силе машине Тьюринга. Три функции выше (плюс ap
) образуют исчисление СКИ, эквивалентную формальную систему.
Можно кодировать любой тип данных Haskell в T
. Рассмотрим тип натуральных чисел
data Nat = Zero | Succ Nat
мы можем кодировать Nat
в T
church :: Nat -> T
church Zero = MkT $ \f -> MkT $ \x -> x
church (Succ n) = MkT $ \f -> MkT $ \x -> f `ap` (church n)
теперь, вы частично правы, хотя. В Haskell нет способа написать обратную функцию этого (насколько я знаю). Это действительно позор. Хотя вы можете написать своего рода psuedo, обратный типу T -> IO Nat
. Кроме того, я понимаю, что оптимизатор GHC может умереть на рекурсивном newtypes
(кто-то, пожалуйста, исправьте меня, если я ошибаюсь в этом, потому что я хотел бы вернуться к их использованию).
Вместо этого тип
data T = MkT (T -> T) | Failed String
с
ap (MkT f) a = f a
ap (Failed s) _ = Failed s
который является исчислением лямбда с исключениями, может быть использован полностью обратимым образом.
В заключение, в некотором смысле T
вообще не является полезным типом, но в другом смысле это самый полезный тип всех.