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 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/8e400cd0-7e87-4a07-a6f0-2aa3c0a362f5%40googlegroups.com.