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
>
> On Saturday, January 13, 2018 at 11:59:38 AM UTC-5, Max Hayden Chiz wrote:
>>
>>
>>
>> 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?
>>
>>>
>>> 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), "")
>>>
>>>
>>>
>>>
>>> On Friday, January 12, 2018 at 11:02:45 PM UTC-5, Max Hayden Chiz wrote:
>>>>
>>>>
>>>>
>>>> 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.
>>>>
>>>>
>>>>
>>>>
>>>>> On Friday, January 12, 2018 at 7:49:45 PM UTC-5, Max Hayden Chiz wrote:
>>>>>>
>>>>>> 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?
>>>>>>
>>>>>>
--
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/93d9768d-e11c-4c0f-8aad-baddc298e59b%40googlegroups.com.
