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

Question

При выражении бесконечных типов в Haskell:

f x = x x -- This doesn't type check

Для этого можно использовать newtype:

newtype Inf = Inf { runInf :: Inf -> * }

f x = x (Inf x)

Существует ли эквивалент newtype для видов, который позволяетодин для выражения бесконечных видов?

Я уже обнаружил, что могу использовать семейства типов, чтобы получить нечто подобное:

{-# LANGUAGE TypeFamilies #-}
data Inf (x :: * -> *) = Inf
type family RunInf x :: * -> *
type instance RunInf (Inf x) = x

Но я не удовлетворен этим решением - в отличие от эквивалентов типов,Inf не создает новый вид (Inf x имеет вид *), поэтому безопасность в нем меньше.

Есть ли более элегантное решение этой проблемы?

Answer 1

Отвечая на:

Как и в схемах рекурсии, я хочу получить способ создания 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))

Обратите внимание, как мы передаем метки *С 1025 * до 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 индексируется функтором формы, а не меткой, но сейчас мне это кажется чище.Подобные решения должны быть приняты, и мне еще предстоит найти наиболее удобный шаблон.Лучшие абстракции для использования вокруг функторов форм все еще нуждаются в исследовании и разработке.

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

Answer 2

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

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 в своем ответе!

Answer 3

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

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

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