I can only outline a way in ATS that more or less matches
the printf example in your message. In ATS, the function PrintfType
can not be defined.
On the other hand, if I understand correctly, your printf code in Idris
would
not be so easy to use if the format string is not a constant. For instance,
I remember seeing an example in K&R where the format string is constructed
at run-time.
abstype string(string)
abstype format(string)
datatype
Format(type) =
|
{a:type}
Number(int -> a) of Format(a)
|
{a:type}
Str(string -> a) of Format(a)
|
{a:type}
Lit(a) of (String, Format(a))
|
End(string) of ()
extern
fun
toFormat
{cs:string}
(string(cs)): Format(format(cs))
extern
fun
printfFmt
{a:type}
(fmt: Format(a), acc: string): a
extern
fun
printf
{cs:string}(fmt: string(cs)): format(cs)
implement
printf(fmt) = printfFmt(toFormat(fmt), "")
On Friday, January 12, 2018 at 11:02:45 PM UTC-5, Max Hayden Chiz wrote:
>
>
>
> 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 ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
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/e072ff28-4ab3-46a2-834d-1a2264aaab46%40googlegroups.com.
