On Friday, January 12, 2018 at 8:15:54 PM UTC-6, gmhwxi wrote:
>
>
> >>But I assume you mean more generally that the idea of having a variadic
> function and parsing the first argument to determine the number of
> additional arguments and their types wasn't useful.
>
> It may be useful. But using %s for string, %c for char, etc. does not
> look like a good design.
>
> >>Is the variadic function capability what is missing in ATS2? If not,
> what is the difference that ATS1 allows it and ATS2 doesn't?
>
> Variadic functions are supported in ATS2.
>
I was under the impression that they could be *called* but not *created* as
part of ATS2, i.e., I couldn't *make* my own variadic function. If that not
right, could you link to an example of how to make one in ATS?
> To support printf, one needs to parse a constant format string. I did not
> implement such a parser in ATS2.
>
What I'm trying to understand is whether this is something that *hasn't*
been done or something that *can't* be done (short of modifying the
compiler). And again, this is just a toy example to help me understand how
ATS differs from Idris. I'm not trying to make the real printf type-safe or
make a good design for a printing library. I'm just trying to translate an
Idris example into ATS so that I can better understand the ATS language.
I'll provide the Idris code below. I want to know if it's possible to do
something similar in ATS and whether it would work with a run-time supplied
format string or if it would only work for compile-time constants.
The way this works in Idris is as follows:
data Format = Number Format
| Str Format
| Lit String Format
| End
PrintfType : Format -> Type
PrintfType (Number fmt) = (i : Int) -> PrintfType fmt
PrintfType (Str fmt) = (str : String) -> PrintfType fmt
PrintfType (Lit str fmt) = PrintfType fmt
PrintfType End = String
printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Number fmt) acc = \i => printfFmt fmt (acc ++ show i)
printfFmt (Str fmt) acc = \str => printfFmt fmt (acc ++ str)
printfFmt (Lit lit fmt) acc = printfFmt fmt (acc ++ lit)
printfFmt End acc = acc
toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: chars) = Number (toFormat chars)
toFormat ('%' :: 's' :: chars) = Str (toFormat chars)
toFormat ('%' :: chars) = Lit "%" (toFormat chars)
toFormat (c :: chars) = case toFormat chars of
Lit lit chars' => Lit (strCons
c lit) chars'
fmt => Lit (strCons c "") fmt
printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))
printf fmt = printfFmt _ ""
Thank you for your help.
> On Friday, January 12, 2018 at 7:49:45 PM UTC-5, Max Hayden Chiz wrote:
>>
>> Thank you again for your reply.
>>
>> On Friday, January 12, 2018 at 5:42:09 PM UTC-6, gmhwxi wrote:
>>>
>>> ATS1 and ATS2 are very similar modulo minor syntactic differences.
>>> There isn't really much point in learning ATS1.
>>>
>>> I did not implement the printf stuff in ATS2 because it was not
>>> particularly
>>> useful.
>>>
>>
>> I agree that printf isn't particularly useful, it was just a toy example
>> that I was playing with.
>>
>> But I assume you mean more generally that the idea of having a variadic
>> function and parsing the first argument to determine the number of
>> additional arguments and their types wasn't useful.
>>
>>
>>> I have to say that 'printf' was a poor idea to start with in the first
>>> place.
>>> There are a lot more types than letters.
>>>
>>> >> So printf "%c %f" is of type "Char -> Double -> String"
>>>
>>> By the say, this is not true printf. The printf supported in ATS1 is a
>>> variadic function
>>> (just like in C).
>>>
>>
>> Is the variadic function capability what is missing in ATS2? If not, what
>> is the difference that ATS1 allows it and ATS2 doesn't?
>>
>>
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/917fd46a-8f90-4923-baf4-1871c66e0bb5%40googlegroups.com.
