> 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? >
My claim is that it is not "easy". Say I have the following calls: printf (foo(0)) 100 printf (foo(1)) "100" foo(0) returns a string containing %d (but not other occurrences of %) foo(1) returns a string containing %s (but not other occurrences of %) In order for the above code to typecheck at compile time, the above properties about 'foo' need to be made known to the typechecker of Idris. I am curious about how this can actually be done in Idris. On Sat, Jan 13, 2018 at 11:59 AM, Max Hayden Chiz <[email protected]> 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/8e400cd0-7e87-4a07-a6f0-2aa3c0a362f5% > 40googlegroups.com > <https://groups.google.com/d/msgid/ats-lang-users/8e400cd0-7e87-4a07-a6f0-2aa3c0a362f5%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAPPSPLpoiipUH8SqzAB5ddetPE6%2BQR5%3DzRHk2SnV21fVp0ff%3Dg%40mail.gmail.com.
