类型同义词的部分应用

Question

我在以下示例中在不饱和类型的同义词方面遇到麻烦：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
module TypeFamilyHackery where
data T k v a = T
type family CollectArgTypes arr where
  CollectArgTypes (a -> b) = (a, CollectArgTypes b)
  CollectArgTypes _ = ()
type family MapReturnType f t where
  MapReturnType f (a -> b) = a -> MapReturnType f b
  MapReturnType f r = f r
type MkT k v = T k v v
-- | Goal:
-- @
--   BuryT Int = T () Int Int
--   BuryT (Bool -> Int) = Bool -> T (Bool, ()) Int Int
--   BuryT (a -> b -> c) = a -> b -> T (a,(b,())) c c
-- @
type BuryT t = MapReturnType (MkT (CollectArgTypes t)) t

，但这对The type synonym 'MkT' should have 2 arguments, but has been given 1抱怨。我可以专门为MkT (CollectArgTypes t)使用CC_3，但是我宁愿它是什么。

由于-XLiberalTypeSynonyms似乎没有交付（为什么？），我可以选择BuryT工作？

Answer 1

LiberalTypeSynonyms通过插入所有"明显"类型定义来工作。为了使您的榜样起作用，它必须

1. 首先将MapReturnType (MkT (CollectArgTypes t)) t视为一些MapReturnType ㄊ t
2. 使用定义MapReturnType f r = f r
，将其直列化为ㄊ t
3. 在这一点上，再次调用ㄊ将提供MkT (CollectArgTypes t) t，这是一个完全完整的同义词，因此没有问题。

，但是步骤2不可能，因为MapReturnType只是不是同义词。要使用MapReturnType f r = f r，编译器首先必须确保r不是函数类型，但确实不知道这一点 - 毕竟是一个完全免费的参数。

因此，编译器实际需要做的是，将MapReturnType的分辨率以及BuryT的分辨率推迟到混凝土使用站点。现在，这可能非常有用，但是它将打开一罐蠕虫。也就是说，在您的程序类型的任何地方，将图灵完整的程序交织在一起非常容易。我认为这是不值得的。