On Saturday, January 13, 2018 at 1:19:54 PM UTC-6, gmhwxi wrote:
>
>
> Since PrintfType can't be an ATS function, is there a more canonical way
>> to do a function like this printf thing in ATS? Or is this just a current
>> limitation of the language?
>>
>
> Given the design of ATS, I see it as a fundamental limitation of ATS.
>
> But useful systems all have limitations :)
>
Thank you for taking the time to explain all of this. It was very helpful.
I'll keep playing with ATS and will let you know if I have any more
questions.
>
> If I am to support 'printf', I would only handle constant format strings.
> Then
> I can write a parsing function parseFmt externally. Then I can write code
> like
>
> val () = printf(##parseFmt("x(int) = %i and y(string) = %s"), 1, "A")
>
I wouldn't really think this is worthwhile. The only reason the Idris
example is interesting is because it lets you do something that's generally
considered unsafe (taking a printf format string from the user) in a safe
way. If you are just dealing with a constant format string, there are
plenty of other, probably better, ways to get things printed.
>
> On Saturday, January 13, 2018 at 11:59:38 AM UTC-5, Max Hayden Chiz wrote:
>>
>>
>>
>> On Saturday, January 13, 2018 at 8:56:02 AM UTC-6, gmhwxi wrote:
>>>
>>> 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.
>>>
>>
>> Although I'm not sure how it works under the hood, the Idris example does
>> work with run-time constructed strings. That was originally what I was
>> trying to figure out: whether the strict separation between statics and
>> dynamics in ATS made this approach constant-only. But then I couldn't
>> figure out how to translate the example.
>>
>> Since PrintfType can't be an ATS function, is there a more canonical way
>> to do a function like this printf thing in ATS? Or is this just a current
>> limitation of the language?
>>
>>>
>>> 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 [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/806d4df4-609f-4ad8-9269-b7a79d2f55e5%40googlegroups.com.
