Документ "Система F с принуждением к равенству типов" от Sulzmann, Chakravarty и Peyton Jones иллюстрирует перевод Haskell newtype в System FC со следующим примером
newtype T = MkT (T -> T)
Как я понимаю, при запрете unsafePerformIO единственными возможными значениями этого типа являются MkT id и MkT undefined из-за параметричности. Мне любопытно, есть ли некоторые фактические применения для этого (или аналогичного) определения.
Параметричность - это значения типов с переменными. 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 вообще не является полезным типом, но в другом смысле это самый полезный тип всех.