Разбор свободных монад

Не каждое значение Example может быть представлено на странице без повторной реализации некоторой части Haskell. Например, return putStrLn имеет тип Example (String -> IO ()), но я не думаю, что имеет смысл пытаться разобрать такое значение Example из файла.

Итак, давайте ограничимся анализом приведенных вами примеров, которые состоят только из вызовов foo и bar, последовательно соединенных с >> (то есть без связывания переменных и без произвольных вычислений)*. Форма Бэкуса-Наура для нашей грамматики выглядит примерно так:

<program> ::= "" | <expr> "\n" <program>
<expr> ::= "foo " <integer> | "bar " <string>

Достаточно просто разобрать наши два типа выражений...

type Parser = Parsec String ()

int :: Parser Int
int = fmap read (many1 digit)

parseFoo :: Parser (Example ())
parseFoo = string "foo " *> fmap foo int

parseBar :: Parser (Example Int)
parseBar = string "bar " *> fmap bar (many1 alphaNum)

... но как мы можем придать тип составу этих двух парсеров?

parseExpr :: Parser (Example ???)
parseExpr = parseFoo <|> parseBar

parseFoo и parseBar имеют разные типы, поэтому мы не можем составить их с помощью <|> :: Alternative f => f a -> f a -> f a. Кроме того, нет никакого способа узнать заранее, какого типа будет программа, которую нам дали: как вы указываете, тип анализируемой программы зависит от значения входной строки. Типы, зависящие от значений, называются зависимыми типами; В Haskell нет надлежащей системы зависимых типов, но она достаточно близка к тому, чтобы мы попытались заставить этот пример работать.

Давайте начнем с того, что заставим выражения по обе стороны от <|> иметь один и тот же тип. Это включает удаление параметра типа Example с помощью количественная оценка существования.†

data Ex a = forall i. Wrap (a i)

parseExpr :: Parser (Ex Example)
parseExpr = fmap Wrap parseFoo <|> fmap Wrap parseBar

Это проверяет тип, но синтаксический анализатор теперь возвращает Example, содержащее значение неизвестного типа. Значение неизвестного типа, конечно, бесполезно, но мы знаем кое-что о параметре Example: это должно быть либо (), либо Int, потому что это возвращаемые типы parseFoo и parseBar. Программирование — это перенос знаний из вашего мозга на страницу, поэтому мы собираемся завершить значение Example небольшим количеством GADT свидетельство, которое при раскрытии покажет вам, было ли a Int или ().

data Ty a where
    IntTy :: Ty Int
    UnitTy :: Ty ()

data (a :*: b) i = a i :&: b i

type Sig a b = Ex (a :*: b)
pattern Sig x y = Wrap (x :&: y)

parseExpr :: Parser (Sig Ty Example)
parseExpr = fmap (\x -> Sig UnitTy x) parseFoo <|>
            fmap (\x -> Sig IntTy x) parseBar

Ty (что-то вроде) одноэлементного представления параметра типа Example во время выполнения. При сопоставлении с образцом на IntTy вы узнаете, что a ~ Int; когда вы сопоставляете шаблон на UnitTy, вы узнаете, что a ~ (). (Информацию можно заставить передаваться другим путем, от типов к значениям, используя классы.) :*:, функтор-продукт объединяет два конструктора типов, обеспечивая равенство их параметров; таким образом, сопоставление с образцом на Ty говорит вам о сопровождающем его Example.

Sig поэтому называется зависимой парой или сигма типом — тип второго компонента пары зависит от значения первого. Это распространенная техника: когда вы стираете параметр типа с помощью квантификации существования, обычно выгодно сделать его восстанавливаемым, объединив время выполнения, представляющее этот параметр.

parseProgram :: Parser (Sig Ty Example)
parseProgram = fmap (foldr1 combine) $ parseExpr `sepBy1` (char '\n')
    where combine (Sig _ val) (Sig ty acc) = Sig ty (val >> acc)