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 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). --Hongwei On Friday, January 12, 2018 at 5:48:48 PM UTC-5, Max Hayden Chiz wrote: > > Thank you for your reply. > > Is there documentation for ATS1 somewhere (since that's what the compiler > is written in)? And is the reason you can't fully do this in ATS2 just > because ATS2 is still under development or is this an intentional > limitation in the language? > > On Friday, January 12, 2018 at 4:14:15 PM UTC-6, gmhwxi wrote: >> >> For the GADT part, please see >> >> https://gist.github.com/doublec/a3cc8f3431cabe9a319c8e7ba27e7890 >> >> The printf stuff is supported in ATS1. If parsing the format string is not >> of the concern, then you can readily do it following the above GADT >> example. >> >> I used to use the name GRDT for GADT. Please see: >> >> http://www.ats-lang.org/Papers.html#GRDT-popl2003 >> >> On Friday, January 12, 2018 at 4:50:35 PM UTC-5, Max Hayden Chiz wrote: >>> >>> I found out about ATS through wikipedia when I was trying to learn about >>> dependent typing and looking for dependently typed programming languages to >>> try. >>> >>> I read the documentation and now I'm trying to do various things to >>> familiarize myself with the language. That said, there are a lot of new >>> concepts and the language isn't exactly ergonomic, so I'm having a hard >>> time of it. But I really like the ideas and want to be more familiar with >>> them so I'll stick with it. If anyone has advice for speeding up my >>> learning of the language and the standard libraries, I'd appreciate the >>> pointers. >>> >>> Right now there are two things I haven't figured out how to do in ATS. >>> >>> 1) How do you do the equivalent of OCaml's GADTs? The website mentions >>> that this is doable, but I don't see how. Can someone provide me with an >>> example? >>> >>> 2) In Brady's Idris book he shows how you can use dependent typing to >>> make a type-safe printf function. It works like this: >>> >>> toFormat turns a String into a "Format" datatype. A type-level function, >>> "PrintfType" turns a Format into a Type. And a Printf helper function takes >>> an argument called "fmt" which is a Format and returns a "PrintfType fmt" >>> type which is a (closure) function that takes the right number and types of >>> inputs and returns a string. >>> >>> So printf "%c %f" is of type "Char -> Double -> String" >>> >>> Is there a way to do something like this in ATS or does the separation >>> of statics and dynamics mean that this doesn't work in ATS? (Or is there >>> some other limitation in the language that prevents this in practice but >>> not in principle?) Even if you can't do it at the level of dynamic printf >>> strings, could you do it at the static level so that as long as the format >>> string was compiled into the code, the type checker would be able to verify >>> correctness? >>> >>> Thanks for any help you can provide. >>> >> -- 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/8aff999b-edb9-46f5-b6de-029315a2f8a7%40googlegroups.com.
