Translating printf example from Cayenne

[Jean-Laurent Huynh]

Hi All,

I just started with Idris and I wanted to translate the printf example from the Cayenne - a language with dependent types paper. I cannot figure out how to get past a unification error. Here is what I have so far:

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]))

and I'm getting the following error:

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

I also asked the question on stackoverflow. I tried to use the with construct without success. I have the feeling that the compiler does not like the overlapping patterns but I don't know. And if that's the case, I don't know how to solve it (I want to match everything except '%'). How can I solve this issue?

Jean-Laurent

[Benjamin Saunders]

I think this is caused by Idris not being smart enough to infer that the _ on line 49 cannot be 'd' or 's' and/or apply that knowledge to normalizing PrintfType fmt. Support for this would certainly be nice to have.

Jean-Laurent

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.