Выражение бесконечных видов

Отвечая на:

Подобно схемам рекурсии, мне нужен способ построения AST, за исключением того, что я хочу, чтобы мои AST могли ссылаться друг на друга, то есть терм может содержать тип (для лямбда-параметра), тип может содержать тип строки в нем и наоборот. Я бы хотел, чтобы AST были определены с помощью внешней фиксированной точки (чтобы можно было иметь «чистые» выражения или выражения, аннотированные типами после вывода типа), но я также хочу, чтобы эти фиксированные точки могли содержать другие типы фиксированные точки (точно так же, как термы могут содержать термы разных типов). Я не вижу, как Fix мне помогает в этом

У меня есть метод, который, возможно, близок к тому, о чем вы просите, с которым я экспериментировал. Это кажется довольно мощным, хотя абстракции вокруг этой конструкции нуждаются в некотором развитии. Суть в том, что существует тип Label, указывающий, откуда продолжится рекурсия.

{-# LANGUAGE DataKinds #-}

import Data.Kind (Type)

data Label = Label ((Label -> Type) -> Type)
type L = 'Label

L — это просто ярлык для создания меток.

Определения с открытой фиксированной точкой относятся к виду (Label -> Type) -> Type, то есть они принимают «функцию интерпретации (типа) метки» и возвращают тип. Я назвал их «функторами формы» и абстрактно назвал их буквой h. Простейший функтор формы — это тот, который не рекурсивно:

newtype LiteralF a f = Literal a  -- does not depend on the interpretation f
type Literal a = L (LiteralF a)

Теперь мы можем сделать небольшую грамматику выражений в качестве примера:

data Expr f
    = Lit (f (Literal Integer))
    | Let (f (L Defn)) (f (L Expr))
    | Var (f (L String))
    | Add (f (L Expr)) (f (L Expr))

data Defn f
    = Defn (f (Literal String)) (f (L Expr))

Обратите внимание, как мы передаем метки в f, который, в свою очередь, отвечает за закрытие рекурсии. Если нам просто нужно нормальное дерево выражений, мы можем использовать Tree:

data Tree :: Label -> Type where
    Tree :: h Tree -> Tree (L h)

Тогда Tree (L Expr) изоморфно обычному дереву выражений, которое вы ожидаете. Но это также позволяет нам, например, аннотировать дерево аннотацией, зависящей от метки, на каждом уровне дерева:

data Annotated :: (Label -> Type) -> Label -> Type where
    Annotated :: ann (L h) -> h (Annotated ann) -> Annotated ann (L h)

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

Есть много других возможностей, многие из которых я не исследовал. Если вы в конечном итоге используете его, я хотел бы услышать о вашем случае использования.

С типами данных мы можем использовать обычный новый тип:

import Data.Kind (Type)

newtype Inf = Inf (Inf -> Type)

И продвигайте его (с помощью '), чтобы создавать новые виды для представления циклов:

{-# LANGUAGE DataKinds #-}

type F x = x ('Inf x)

Чтобы тип распаковал свой аргумент 'Inf, нам нужно семейство типов:

{-# LANGUAGE TypeFamilies #-}

type family RunInf (x :: Inf) :: Inf -> Type
type instance RunInf ('Inf x) = x

Теперь мы можем выражать бесконечные виды с помощью нового вида для них, так что ни одна безопасность вида не будет потеряна.

• Спасибо @luqui за то, что указал на часть DataKinds в своем ответе!

Я думаю, вы ищете Fix, который определяется как

data Fix f = Fix (f (Fix f))

Fix дает вам фиксированную точку типа f. Я не уверен, что вы пытаетесь сделать, но такие бесконечные типы обычно используются, когда вы используете схемы рекурсии (шаблоны рекурсии, которые вы можете использовать), см. пакет recursion-schemes Эдварда Кметта или бесплатные монады, которые, среди прочего, позволяют вам построить AST в монадическом стиле.