Зависимо типизированный printf в Idris

Я пытаюсь перевести на Идрис пример из Cayenne — языка с зависимыми типами бумага.

Вот что у меня есть до сих пор:

PrintfType : (List Char) -> Type
PrintfType Nil                = String
PrintfType ('%' :: 'd' :: cs) = Int -> PrintfType cs
PrintfType ('%' :: 's' :: cs) = String -> PrintfType cs
PrintfType ('%' ::  _  :: cs) = PrintfType cs
PrintfType ( _  :: cs)        = PrintfType cs

printf : (fmt: List Char) -> PrintfType fmt
printf fmt = rec fmt "" where
  rec : (f: List Char) -> String -> PrintfType f
  rec Nil acc = acc
  rec ('%' :: 'd' :: cs) acc = \i => rec cs (acc ++ (show i))
  rec ('%' :: 's' :: cs) acc = \s => rec cs (acc ++ s) 
  rec ('%' ::  _  :: cs) acc = rec cs acc  -- this is line 49
  rec ( c  :: cs)        acc = rec cs (acc ++ (pack [c]))

Я использую List Char вместо String для аргумента format, чтобы облегчить сопоставление с образцом, поскольку я быстро столкнулся со сложностью сопоставления с образцом на String.

К сожалению, я получаю сообщение об ошибке, которое не могу понять:

Type checking ./sprintf.idr
sprintf.idr:49:Can't unify PrintfType (Prelude.List.:: '%' (Prelude.List.:: t cs)) with PrintfType cs

Specifically:
    Can't convert PrintfType (Prelude.List.:: '%' (Prelude.List.:: t cs)) with PrintfType cs

Если я закомментирую все случаи совпадения с шаблоном с 3 элементами (те, что с '%' :: ...) в PrintfType и printf, то код компилируется (но, очевидно, не делает ничего интересного).

Как исправить мой код, чтобы printf "the %s is %d" "answer" 42 работало?


idris
person huynhjl    schedule 28.07.2013    source источник

Ответы (1)


arrow_upward
14
arrow_downward

Похоже, в idris есть некоторые текущие ограничения при определении функций, в которых шаблоны перекрываются ( например '%' :: 'd' перекрывается с c :: cs После многих попыток я наконец нашел обходной путь для этого:

data Format = End | FInt Format | FString Format | FChar Char Format
fromList : List Char -> Format
fromList Nil                = End
fromList ('%' :: 'd' :: cs) = FInt    (fromList cs)
fromList ('%' :: 's' :: cs) = FString (fromList cs)
fromList (c :: cs)          = FChar c (fromList cs)

PrintfType : Format -> Type
PrintfType End            = String
PrintfType (FInt rest)    = Int -> PrintfType rest
PrintfType (FString rest) = String -> PrintfType rest
PrintfType (FChar c rest) = PrintfType rest

printf : (fmt: String) -> PrintfType (fromList $ unpack fmt)
printf fmt = printFormat (fromList $ unpack fmt) where
  printFormat : (fmt: Format) -> PrintfType fmt
  printFormat fmt = rec fmt "" where
    rec : (f: Format) -> String -> PrintfType f
    rec End acc            = acc
    rec (FInt rest) acc    = \i: Int => rec rest (acc ++ (show i))
    rec (FString rest) acc = \s: String => rec rest (acc ++ s)
    rec (FChar c rest) acc = rec rest (acc ++ (pack [c]))

Format — это рекурсивный тип данных, представляющий строку формата. FInt — это заполнитель типа int, FString — строковый заполнитель, а FChar — символьный литерал. Используя Format, я могу определить PrintfType и реализовать printFormat. Оттуда я могу плавно перейти к строке, а не к значению List Char или Format. И конечный результат:

*sprintf> printf "the %s is %d" "answer" 42
"the answer is 42" : String
person huynhjl    schedule 01.08.2013
comment
Какие доказательства вам нужно предоставить, чтобы этот printf работал со строкой времени выполнения? - person is7s; 24.11.2014
comment
@is7s, хороший вопрос, не знаю. Я не играл с Идрисом после этого вопроса/ответа. Я вижу некоторую идею в eb.host.cs. st-andrews.ac.uk/drafts/eff-tutorial.pdf, где сказано вернуть доказательство того, что целое число находится в требуемом диапазоне вместе с самим целым числом. Итак, я думаю, вам придется проанализировать строку формата и вернуть ее с доказательством, которое имеет некоторые Format. - person huynhjl; 25.11.2014