Here is another example using GADTs: https://groups.google.com/forum/#!msg/ats-lang-users/tfEnAR2vIOA/0LyuBqMaBAAJ;context-place=topic/ats-lang-users/MK-VrrpthCU
On Friday, January 12, 2018 at 5:14:15 PM UTC-5, 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/1e7fbb4f-3a73-4ad5-ab7b-5279b04e46e3%40googlegroups.com.
