Развитие структуры данных - программирование

Я пытаюсь написать компилятор для C-подобного языка в Haskell. Компилятор развивается путем преобразования АСТ. Первый проход анализирует ввод для создания АСТ, связывая узел с таблицей символов, чтобы позволить размещать символы до того, как они были определены без необходимости прямых ссылок.

AST содержит информацию о типах и выражениях, и между ними могут быть связи; например sizeof(T) - это выражение, которое зависит от типа T, а T[e] - тип массива, который зависит от постоянного выражения e.

Типы и выражения представлены типами данных Haskell, например:

Где Unop включает в себя такие операторы, как address-of (&) и разыменование (*), а Binop включает в себя такие операторы, как plus (+) и times (*), и т.д....

Обратите внимание, что каждому типу присваивается уникальный Id. Это используется для построения графа зависимости типа для обнаружения циклов, приводящих к бесконечным типам. Как только мы уверены, что в графе типов нет циклов, безопасно применять к ним рекурсивные функции, не входя в бесконечный цикл.

Следующий шаг - определить размер каждого типа, назначить смещения для структурных полей и заменить ExprField на арифметику указателя. При этом мы можем определить тип выражений и исключить ExprSizeof s, ExprField s, TypeDef s и TypeOf из графа типов, поэтому наши типы и выражения эволюционировали, а теперь выглядят более например:

Обратите внимание, что мы устранили некоторые из конструкторов данных и немного изменили некоторые из других. В частности, Type' больше не содержит Expr', и каждый Expr' определил его Type'.

Итак, наконец, вопрос: лучше ли создавать два почти одинаковых набора типов данных или пытаться объединить их в один тип данных?

Сохранение двух отдельных типов данных делает его явным, что некоторые конструкторы больше не отображаются. Однако функция, которая выполняет постоянную фальцовку для оценки постоянных выражений, будет иметь тип:

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

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

Кроме того, что мы помещаем в неизвестные поля (например, смещения полей, размеры массивов и типы выражений) во время первого прохода? Мы могли бы подключить отверстия с помощью undefined или error "*hole*", но это похоже на то, что произойдет ожидание (например, NULL указатели, которые вы даже не можете проверить). Мы могли бы изменить неизвестные поля на Maybe s и подключить отверстия с помощью Nothing (например, указателей NULL, которые мы можем проверить), но в последующих проходах было бы раздражать необходимость вытягивать значения из Maybe, которые всегда будут Just s.

Ответы

Ответ 1

Надеюсь, у кого-то, у кого больше опыта, будет более отполированный, проверенный на битву и готовый ответ, но вот мой выстрел в него.

Вы можете получить свой пирог и съесть его часть при относительно небольших затратах с помощью GADT:

{-# LANGUAGE GADTs #-}

data P0 -- phase zero
data P1 -- phase one

data Type p where
     TypeInt     :: Id -> Type p
     TypePointer :: Id -> Type p -> Type p             -- target type
     TypeArray   :: Id -> Type p -> Expr p -> Type p   -- elt type, elt count
     TypeStruct  :: Id -> [(String, Type p)] -> Type p -- [(field name, field type)]
     TypeOf      :: Id -> Expr P0 -> Type P0
     TypeDef     :: Id -> Type P0 -> Type P0

data Expr p where
     ExprInt     :: Int -> Expr p                        -- literal int
     ExprVar     :: Var -> Expr p                        -- variable
     ExprSizeof  :: Type P0 -> Expr P0
     ExprUnop    :: Unop -> Expr p -> Expr p
     ExprBinop   :: Binop -> Expr p -> Expr p -> Expr p
     ExprField   :: Bool -> Expr P0 -> String -> Expr P0 -- Bool gives true=>s.field, false=>p->field

Здесь мы изменили следующие вещи:

Теперь типы данных используют синтаксис GADT. Это означает, что конструкторы объявляются с использованием их сигнатур типа. data Foo = Bar Int Char становится data Foo where Bar :: Int -> Char -> Foo (кроме синтаксиса, они полностью эквивалентны).
Мы добавили переменную типа для Type и Expr. Это так называемая переменная типа phantom: нет фактических данных, которые имеют тип p, он используется только для обеспечения инвариантов в системе типов.
Мы объявили фиктивные типы для представления фаз до и после преобразования: фаза нуля и первая фаза. (В более сложной системе с несколькими фазами мы могли бы использовать номера типов типов для их обозначения.)
GADT позволяют хранить инварианты уровня типа в структуре данных. Здесь у нас есть два из них. Во-первых, рекурсивные позиции должны быть той же фазы, что и структура, содержащая их. Например, глядя на TypePointer :: Id -> Type p -> Type p, вы передаете конструктор Type p в конструктор TypePointer и получаете результат Type p, а те p должны быть одного типа. (Если бы мы хотели разрешить разные типы, мы могли бы использовать p и q.)
Во-вторых, мы применяем тот факт, что некоторые конструкторы могут использоваться только в первой фазе. Большинство конструкторов являются полиморфными в переменной типа phantom p, но некоторые из них требуют, чтобы она была P0. Это означает, что эти конструкторы могут использоваться только для построения значений типа Type P0 или Expr P0, а не для любой другой фазы.

GADT работают в двух направлениях. Во-первых, если у вас есть функция, которая возвращает Type P1, и попытайтесь использовать один из конструкторов, который возвращает Type P0 для его создания, вы получите ошибку типа. Это то, что называется "правильным по построению": статически невозможно построить недопустимую структуру (при условии, что вы можете кодировать все соответствующие инварианты в системе типов). Оборотная сторона этого заключается в том, что если у вас есть значение Type P1, вы можете быть уверены, что оно было построено правильно: конструкторы TypeOf и TypeDef не могли быть использованы (на самом деле компилятор будет жаловаться если вы попытаетесь совместить их с шаблоном), и любые рекурсивные позиции также должны иметь фазу P1. По сути, когда вы создаете GADT, вы храните доказательства того, что ограничения типа удовлетворяются, и когда вы сопоставляете шаблон с ним, вы извлекаете это свидетельство и можете воспользоваться им.

Это была легкая часть. К сожалению, у нас есть некоторые различия между двумя типами, кроме тех, которые разрешены конструкторами: некоторые из аргументов конструктора различаются между фазами, а некоторые из них присутствуют только в фазе после преобразования. Мы можем снова использовать GADT для кодирования этого, но это не так дешево и элегантно. Одним из решений было бы дублирование всех конструкторов, которые отличаются друг от друга, и каждый из них имеет значение P0 и P1. Но дублирование не очень приятно. Мы можем попытаться сделать это более мелкозернистым:

-- a couple of helper types
-- here I take advantage of the fact that of the things only present in one phase,
-- they're always present in P1 and not P0, and not vice versa
data MaybeP p a where
     NothingP :: MaybeP P0 a
     JustP    :: a -> MaybeP P1 a

data EitherP p a b where
     LeftP  :: a -> EitherP P0 a b
     RightP :: b -> EitherP P1 a b

data Type p where
     TypeInt     :: Id -> Type p
     TypePointer :: Id -> Type p -> Type p
     TypeArray   :: Id -> Type p -> EitherP p (Expr p) Int -> Type p
     TypeStruct  :: Id -> [(String, MaybeP p Int, Type p)] -> Type p
     TypeOf      :: Id -> Expr P0 -> Type P0
     TypeDef     :: Id -> Type P0 -> Type P0

-- for brevity
type MaybeType p = MaybeP p (Type p)

data Expr p where
     ExprInt     :: MaybeType p -> Int -> Expr p
     ExprVar     :: MaybeType p -> Var -> Expr p
     ExprSizeof  :: Type P0 -> Expr P0
     ExprUnop    :: MaybeType p -> Unop -> Expr p -> Expr p
     ExprBinop   :: MaybeType p -> Binop -> Expr p -> Expr p -> Expr p
     ExprField   :: Bool -> Expr P0 -> String -> Expr P0

Здесь с некоторыми вспомогательными типами мы применяем тот факт, что некоторые аргументы конструктора могут присутствовать только в первой фазе (MaybeP), а некоторые разные между двумя фазами (EitherP). Хотя это делает нас совершенно безопасными по типу, он чувствует себя немного ad-hoc, и нам все равно приходится все время перематывать вещи из MaybeP и EitherP. Я не знаю, есть ли лучшее решение в этом отношении. Однако полная безопасность типов - это то, что мы могли бы написать fromJustP :: MaybeP P1 a -> a и убедиться, что она полностью и полностью безопасна.

Обновление: альтернативой является использование TypeFamilies:

data Proxy a = Proxy

class Phase p where
    type MaybeP  p a
    type EitherP p a b
    maybeP  :: Proxy p -> MaybeP p a -> Maybe a
    eitherP :: Proxy p -> EitherP p a b -> Either a b
    phase   :: Proxy p
    phase = Proxy

instance Phase P0 where
    type MaybeP  P0 a   = ()
    type EitherP P0 a b = a
    maybeP  _ _ = Nothing
    eitherP _ a = Left a

instance Phase P1 where
    type MaybeP  P1 a   = a
    type EitherP P1 a b = b
    maybeP  _ a = Just  a
    eitherP _ a = Right a

Единственное изменение в Expr и Type относительно предыдущей версии заключается в том, что конструкторы должны иметь добавленное ограничение Phase p, например. ExprInt :: Phase p => MaybeType p -> Int -> Expr p.

Здесь, если известен тип p в Type или Expr, вы можете статически узнать, будет ли MaybeP () или заданным типом, а какой тип - EitherP являются и могут использовать их непосредственно в качестве этого типа без явной развертки. Когда p неизвестно, вы можете использовать MaybeP и EitherP из класса Phase, чтобы узнать, что они собой представляют. (Аргументы Proxy необходимы, поскольку в противном случае у компилятора не было бы возможности указать, какую фазу вы имели в виду.) Это аналогично версии GADT, где, если p известно, вы можете быть уверены в том, что MaybeP и EitherP, в противном случае вы должны сопоставить оба варианта. Это решение не является совершенным ни в том смысле, что "отсутствующие" аргументы становятся (), а не полностью исчезают.

Построение Expr и Type также, по-видимому, в целом сходно между двумя версиями: если значение, которое вы создаете, имеет что-то конкретное по фазе, оно должно указывать эту фазу в своем типе. Проблема возникает, когда вы хотите написать функцию polyorphic в p, но все же обрабатывать фазовые части. С GADT это просто:

asdf :: MaybeP p a -> MaybeP p a
asdf NothingP  = NothingP
asdf (JustP a) = JustP a

Обратите внимание, что если бы я просто написал asdf _ = NothingP, компилятор пожаловался бы, потому что тип вывода не гарантировался бы таким же, как и вход. По сопоставлению с образцом мы можем выяснить, какой тип ввода и вернуть результат того же типа.

Однако с версией TypeFamilies это намного сложнее. Просто используя MaybeP и результирующий Maybe, вы ничего не сможете доказать компилятору о типах. Вы можете получить часть пути туда вместо MaybeP и EitherP return Maybe и Either, создавая им функции деконструктора, такие как Maybe и Either, которые также предоставляют доступность типа:

maybeP  :: Proxy p -> (p ~ P0 => r) -> (p ~ P1 => a -> r) -> MaybeP p a -> r
eitherP :: Proxy p -> (p ~ P0 => a -> r) -> (p ~ P1 => b -> r) -> EitherP p a b -> r

(Заметим, что для этого нам нужно Rank2Types, и также обратите внимание, что это, по существу, CPS-преобразованные версии версий GADT MaybeP и EitherP.)

Тогда мы можем написать:

asdf :: Phase p => MaybeP p a -> MaybeP p a
asdf a = maybeP phase () id a

Но этого все еще недостаточно, потому что GHC говорит:

data.hs:116:29:
 Could not deduce (MaybeP p a ~ MaybeP p0 a0)
 from the context (Phase p)
   bound by the type signature for
              asdf :: Phase p => MaybeP p a -> MaybeP p a
   at data.hs:116:1-29
 NB: `MaybeP' is a type function, and may not be injective
 In the fourth argument of `maybeP', namely `a'
 In the expression: maybeP phase () id a
 In an equation for `asdf': asdf a = maybeP phase () id a

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

Обновление снова: проблема заключалась в том, что, поскольку MaybeP p a является функцией типа, и никакой другой информации не существует, GHC не может знать, что должно быть p и a. Если я передаю в Proxy p и использую это вместо Phase, который решает p, но a пока неизвестен.

Ответ 2

Нет идеального решения этой проблемы, поскольку у каждого есть разные плюсы и минусы.

Я лично хотел бы использовать одно дерево данных и добавить отдельные конструкторы данных для вещей, которые нужно дифференцировать. То есть:.

data Type
  = ...
  | TypeArray Id Type Expr
  | TypeResolvedArray Id Type Int
  | ...

Это имеет то преимущество, что вы можете запускать одну и ту же фазу несколько раз на одном и том же дереве, как вы говорите, но рассуждения идут глубже: пусть говорят, что вы реализуете синтаксический элемент, который генерирует больше АСТ (что-то вроде include или тип сделки с С++, и он может зависеть от постоянных exprs, таких как ваш TypeArray, чтобы вы не могли оценить его на первой итерации). С помощью унифицированного подхода типа данных вы можете просто вставить новый AST в существующее дерево, и вы можете не только запустить те же фазы, что и раньше, в этом дереве, но вы получите бесплатное кеширование, то есть, если новый AST ссылается на массив с помощью sizeof(typeof(myarr)) или что-то еще, вам не нужно снова определять постоянный размер myarr, потому что его тип уже является TypeResolvedArray из вашей предыдущей фазы разрешения.

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

Кстати, вы должны использовать Data.Word.Word вместо Data.Int.Int для размеров массива. Это такая распространенная ошибка в C, чтобы использовать int для индексирования массивов, в то время как C-указатели фактически не обозначены. Пожалуйста, не делайте эту ошибку и на своем языке, если вы действительно не хотите поддерживать массивы с отрицательными размерами.