How to do type-safe printf and GADT in ATS?

[Max Hayden Chiz]

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.

[gmhwxi]

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

[gmhwxi]

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

[Max Hayden Chiz]

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?

[gmhwxi]

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

[Max Hayden Chiz]

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?

[gmhwxi]

>>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.

To support printf, one needs to parse a constant format string. I did not implement such a parser in ATS2.

[Max Hayden Chiz]

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.

[gmhwxi]

You are right.

As of now, variadic functions can be implemented in ATS1
but not in ATS2. One can do something as follows, though:

#include
"share/atspre_staload.hats"
#include
"share/atspre_staload_libats_ML.hats"

datatype tag(t@ype) =
  | T1(int) | T2(@(int, string))

extern
fun{a:t@ype} foo(tag(a), a): void


implement
foo<int>(tag, data) =
(
case- tag of T1() => print_int(data)
)
implement
foo<(int,string)>(tag, data) =
(
case- tag of T2() => (print_int(data.0); print_string(data.1))
)

val () = foo(T1(), 1)
val () = foo(T2(), @(1, "A"))

implement main0() = ((*void*))

[gmhwxi]

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.

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), "")

[Max Hayden Chiz]

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?

[gmhwxi]

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.

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.

[Max Hayden Chiz]

On Saturday, January 13, 2018 at 11:18:14 AM UTC-6, gmhwxi wrote:

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.

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.

I'm far from an expert at this as I'm still learning to *use* dependent types let alone design languages with them.

I see what you are saying though. And it does strike me as kind of mysterious. (In fact part of the reason I started playing with ATS is that I couldn't understand what Idris was doing under the hood to make my code work.) If it helps, AFAIK, foo has to be a total function. So it could just calculate foo(0) at compile time in your example.

But that doesn't really resolve the question because it can typecheck even if you read foo's argument from user input at run-time and then take the other arguments for printf from the user and validate them before running it. My thought is that in the latter case, it is actually somehow proving that the validation code obeys the strictures of the type system. Also, as I understand it, there's no guarantee that the type-level code won't execute at run-time. It will use type-erasure wherever it can to eliminate unnecessary variables and functions at the type level, but if it can't, it will just run them as if they were value-level code. So that might relax the requirements of what it has to prove in practice.

There's an extended example in chapter 6 of Brady's book where he builds an interactive data store that allows the user to input the type schema and then use that scheme to construct and manipulate a data store in a type checked manner.

So a session could look like this:

Command: schema String String Int

OK

Command: add "Rain Dogs" "Tom Waits" 1985

ID 0

Command: add "Fog on the Tyne" "Lindisfarne" 1971

ID 1

Command: get 1

"Fog on the Tyne", "Lindisfarne", 1971

Command: quit

[gmhwxi]

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?

Given the design of ATS, I see it as a fundamental limitation of ATS.

But useful systems all have limitations :)

If I am to support 'printf', I would only handle constant format strings. Then
I can write a parsing function parseFmt externally. Then I can write code like

val () = printf(##parseFmt("x(int) = %i and y(string) = %s"), 1, "A")

[gmhwxi]

I see what you are saying though. And it does strike me as kind of mysterious. (In fact part of the reason I started playing with ATS is that I couldn't understand what Idris was doing under the hood to make my code work.) If it helps, AFAIK, foo has to be a total function. So it could just calculate foo(0) at compile time in your example.

I think I have a reasonable grasp of what is going under the hood.

ATS uses a fundamentally different design. To me, a very big concern
here is that one has to have access to the implementation of 'foo' (not just its type)
in order to typecheck the aforementioned code.

[Max Hayden Chiz]

On Saturday, January 13, 2018 at 1:19:54 PM UTC-6, gmhwxi wrote:

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?

Given the design of ATS, I see it as a fundamental limitation of ATS.

But useful systems all have limitations :)

Thank you for taking the time to explain all of this. It was very helpful.

I'll keep playing with ATS and will let you know if I have any more questions.

 

If I am to support 'printf', I would only handle constant format strings. Then
I can write a parsing function parseFmt externally. Then I can write code like

val () = printf(##parseFmt("x(int) = %i and y(string) = %s"), 1, "A")

I wouldn't really think this is worthwhile. The only reason the Idris example is interesting is because it lets you do something that's generally considered unsafe (taking a printf format string from the user) in a safe way.  If you are just dealing with a constant format string, there are plenty of other, probably better, ways to get things printed.