Комбинатор парсеров Idris GADT

В настоящее время я работаю над реализацией простой библиотеки комбинатора синтаксического анализатора в Идрисе, чтобы изучить язык и лучше понять системы типов в целом, но у меня возникли некоторые проблемы с пониманием того, как объявляются и используются GADT. Тип данных парсера, который я пытаюсь сформулировать, выглядит (в Haskell): type Parser a = String -> [(a,String)], from этот документ. По сути, тип - это функция, которая принимает строку и возвращает список.

В Идрисе у меня есть:

data Parser : Type -> Type where
    fail : a -> (String -> [])
    pass : a -> (String -> [(a,String)])

где экземпляр fail - это синтаксический анализатор, который всегда дает сбой (т.е.- будет функцией, которая всегда возвращает пустой список), а экземпляр pass - это синтаксический анализатор, который использовал какой-либо символ. При загрузке вышеуказанного в интерпретатор я получаю сообщение об ошибке несоответствия типа между List elem и ожидаемым типом Type. Но когда я проверяю возвращаемый тип синтаксического анализатора в ответе с помощью :t String -> List Type, я получаю Type, что похоже, что он должен работать.

Я был бы очень благодарен, если бы кто-нибудь мог дать хорошее объяснение, почему это объявление данных не работает, или лучшую альтернативу представлению типа данных парсера.


types parsing gadt idris
person vikingsheepman    schedule 19.03.2016    source источник

Ответы (2)


arrow_upward
2
arrow_downward

В Haskell,

type Parser a = String -> [(a,String)]

не создает новый тип, это просто синоним типа. Вы можете сделать что-то подобное в Идрисе как

Parser : Type -> Type
Parser a = String -> List (a, String)

а затем определите свои вспомогательные определения как простые функции, возвращающие Parser as:

fail : Parser a
fail = const []

pass : a -> Parser a
pass x = \s => [(x, s)]
person Cactus    schedule 21.03.2016
comment
Спасибо, это именно то, что я искал. Не могли бы вы объяснить или указать на ресурс для ->, которого нет в сигнатуре типа? Я не знал, что стрелки можно использовать вне деклараций типов. - person vikingsheepman; 21.03.2016
comment
=> - это просто синтаксис Idris для лямбда-выражений: то, что в Haskell будет \x -> e, в Idris записано как \x => e. - person Cactus; 22.03.2016
comment
Извините, надо было быть более ясным. Я имел в виду строку Parser a = String -> List (a, String). Создает ли -> в этой строке тип, являющийся функцией? И означает ли -> одно и то же, независимо от того, встречается ли это в сигнатуре типа или в определении функции? - person vikingsheepman; 22.03.2016
comment
Это в точности то же самое, что сказать type Parser a = String -> LIst (a, String) в Haskell: он не определяет новый тип, а просто вводит синоним типа. - person Cactus; 22.03.2016
comment
Сложность заключается в том, что Parser - это функция, которая принимает в качестве аргумента Type и в результате возвращает другой Type. Это похоже на конструктор типа * -> * в Haskell; но в Идрисе ее не нужно определять каким-либо образом, кроме функции, которая принимает, скажем, аргумент типа Int и возвращает Bool. - person Cactus; 22.03.2016

arrow_upward
2
arrow_downward

При определении вашего парсера типа данных первая строка говорит, что этот тип принимает тип и возвращает тип, в этом случае он принимает a и возвращает Parser a.

Итак, ваши конструкторы должны возвращать Parser a.

Подобно List, который принимает a и возвращает List a.

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

Однако, помимо этого, я не уверен, как вы лучше всего это изобразите. Однако есть несколько библиотек парсеров, уже написанных на Idris, их просмотр может помочь? Например, взгляните на этот список библиотек, парсеры упомянуты первыми: - Библиотеки Идриса

person guraaku    schedule 20.03.2016