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/6de8b1a1-5816-4d6b-9271-8c5056bd426d%40googlegroups.com.
