Ограничение роста деревьев: семейства типов и классы типов

В вашем случае (Lamfam χ) -> (Arrfam χ) неоднозначно, потому что нет гарантии, что либо Lamfam χ, либо Arrfam χ достаточно, чтобы сказать, какой χ вы хотите на месте вызова. Например, только что проанализированный AST без аннотаций может установить для них оба значения data SrcLoc.

Здесь нет проблем с AllowAmbiguousTypes. В нем говорится, что вы соглашаетесь писать аннотации типа или TypeApplications иногда на сайтах звонков. Вы можете сделать эти семейства типов инъективными, используя TypeFamilyDependencies аннотации:

type family Lamfam χ = λ | λ -> χ

Неявно, семейство типов должно быть функцией, вход которой χ однозначно определяет его вывод λ. Это просто добавляет зависимость в другом направлении, что для любого вывода λ, полученного из приложения Lamfam χ, должно быть достаточно, чтобы сказать, каким был ввод χ. Это довольно строгое требование, которое сводит на нет некоторые предполагаемые преимущества TTG (избегание типов-оболочек). Также есть некоторые проблемы с выразительностью проверки инъективности в текущем GHC. Тем не менее, когда он работает, вывод и сообщения об ошибках становятся более полезными. Распространенной идиомой для создания инъективного семейства является сохранение входного типа в качестве параметра фантомного типа. В основном, замените такие вещи:

newtype Name = Name String
newtype Id   = Id   Int

type family Namefam χ
type instance Namefam Parsed  = Name
type instance Namefam Renamed = Id    -- conflict
type instance Namefam Typed   = Id    -- conflict

С такими вещами:

newtype Name  = Name String
newtype Id' χ = Id'  Int
-- or: Const Id χ

type family Namefam χ
type instance Namefam 'Parsed      = Name
type instance Namefam 'Renamed     = Id' 'Renamed
type instance Namefam 'Typechecked = Id' 'Typechecked

Однако это немного сбивает с толку. Обычно с TTG средство проверки типов не будет полиморфным в χ, оно изменит χ с 'Renamed на 'Typechecked, реаннотируя дерево. В этом случае у вас есть конкретные доступные типы, и вам не нужен класс типов.

Ваш class Checker χ описывает только набор состояний AST, в которых у вас достаточно информации для запуска проверки типов. Так что я не знаю, действительно ли она имеет значение как абстракция, если только вы не хотите иметь возможность повторно проверять тип программы между проходами, скажем, чтобы убедиться, что ничего не было нарушено переписыванием.

Тем не менее, в GHC есть одно примечательное решение проблемы больших наборов ограничений, которое может оказаться полезным. Во-первых, они начинаются с типа Pass для индексации результата каждого прохода.

data Pass
  = Parsed
  | Renamed
  | Typechecked

(Их всего несколько, потому что сейчас они используют TTG только для внешнего интерфейса, но если вы пишете компилятор, использующий TTG с самого начала, вы, безусловно, можете использовать его для большей части конвейера.)

Далее, вместо прямого индексирования AST и точек расширения с этим типом, например HsExpr 'Parsed, они используют GADT GhcPass (например, Sing Pass с singletons).

data GhcPass (c :: Pass) where
  GhcPs :: GhcPass 'Parsed
  GhcRn :: GhcPass 'Renamed
  GhcTc :: GhcPass 'Typechecked

-- Type synonyms as a shorthand for tagging
type GhcPs   = GhcPass 'Parsed      -- Output of parser
type GhcRn   = GhcPass 'Renamed     -- Output of renamer
type GhcTc   = GhcPass 'Typechecked -- Output of typechecker

Наконец, они добавляют класс IsPass (например, SingI или KnownNat), который позволяет унифицировать диспетчеризацию по типу.

class IsPass p where
  ghcPass :: GhcPass p

instance IsPass 'Parsed where
  ghcPass = GhcPs

instance IsPass 'Renamed where
  ghcPass = GhcRn

instance IsPass 'Typechecked where
  ghcPass = GhcTc

Это используется особенно для красивой печати, а иногда и для построения деревьев. Это означает, что вместо того, чтобы носить с собой набор всех ограничений, которые им могут понадобиться, как в ForAllχ c χ, они могут использовать IsPass p => HsExpr (GhcPass p). С χ, предоставленным сопоставлением с образцом, каждый c χ становится доступным. Примечательно, что вы даже можете использовать такие ограничения по мере необходимости, без какого-либо конкретного класса:

pprIfPs :: forall p. IsPass p => (p ~ 'Parsed => SDoc) -> SDoc
pprIfPs pp = case ghcPass @p of
  GhcPs -> pp
  _ -> empty

Если вы хотите написать много кода с полиморфной передачей, я считаю, что гораздо проще и понятнее использовать семейство данных или GADT вместо TTG. Сообщения компилятора гораздо полезнее, и есть больше инструментов для сокращения шаблонов, таких как StandaloneDeriving.