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/43552825-82ff-4716-9fd0-77d4047cdf07%40googlegroups.com.
