[Question] In far future, can ATS2 compiler decide dependent types using Higher-Order Model Checking?

[Kiwamu Okabe]

Hi all,

Today, I read some issues on http://www-kb.is.s.u-tokyo.ac.jp/~koba/.
I'm interested in Higher-Order Model Checking, because I think it might
automatically assign dependent types on ATS2 code.

In far future, can ATS2 compiler decide dependent types using
Higher-Order Model Checking?

Thank's,
--
Kiwamu Okabe at METASEPI DESIGN

[gmhwxi]

Because programs (e.g., Linux OS) are written by programmers,
it is only natural that we ask the question: How should programs be written?

Let's say that you want to apply Higher-Order model checking (or something else)
to some code. Where does your code come from in the first place?

To me, types in ATS are primarily for *guiding* programmers to write programs.
In other words, types are like a blueprint and coding is like building according to the
blueprint. For instance, we just had such a simple example:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATS-QA-LIST/qa-list-2015-01-03.dats

I often say that program verification in ATS is program-first and programmer-centric.

It is program-first because the type system of ATS is primarily designed to first guide
the construction of a program.

It is programmer-centric because the validity of a lemma is to be explained by the person
who introduces it. While there is support for theorem-proving in ATS, the support is only secondary.

[gmhwxi]

Certainly, there are many uses of types.

For applying higher-order model-checking, I think that you need a context
and this context is provided by the programmer.

Here is a speculated scenario:

extern
fun foo: some-type // provided by the programmer
implement
foo (x) = let
//
fun bar (y, z) = ... // using higher-order model-checking to synthesize the type of bar
//
in
  ...bar(y, z)...
end // end of [foo]

Basically, the idea is to use higher-model checking to synthesize a type for the inner function
[bar] that can be used to typecheck the implementation of [foo]. This sounds like an interesting
topic for a paper :)

Are you familiar with liquid type (logically qualified types)?

[Hongwei Xi]

---------- Forwarded message ----------
From: Zhiqiang Ren <aren@...>
Date: Tue, Jan 6, 2015 at 3:09 AM
Subject: Re: [ats-lang-users] [Question] In far future, can ATS2 compiler decide dependent types using Higher-Order Model Checking?

Can I understand it in this way? That is type synthesizing is pointless if there is no context enclosing it. Ultimately, such context exists in our mind, which is the design requirement. We can manually inspect the synthesized type. If the synthesized type satisfies the context, then we say the corresponding implementation is good. If such context is encoded as types as well, then the inspection process can be automated.

------------------------------------------------------------------------------
Dive into the World of Parallel Programming! The Go Parallel Website,
sponsored by Intel and developed in partnership with Slashdot Media, is your
hub for all things parallel software development, from weekly thought
leadership blogs to news, videos, case studies, tutorials and more. Take a
look and join the conversation now. http://goparallel.sourceforge.net
_______________________________________________
ats-lang-users mailing list
ats-lan...@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/ats-lang-users

--

Zhiqiang Ren

 

Department of Computer Science

Boston University

[Hongwei Xi]

What I should really say is that the type system of ATS is too broad a context for type synthesis.

However, one should be able to find meaningful type subsytems in ATS that can accommodate practical
type synthesis (based on model-checking or something else).

[Kiwamu Okabe]

Hi Hongwei,
# It's a just chat.

On Tue, Jan 6, 2015 at 11:06 AM, gmhwxi <gmh...@gmail.com> wrote:
> Because programs (e.g., Linux OS) are written by programmers,

> it is only natural that we ask the question: How programs should be written?

>
> Let's say that you want to apply Higher-Order model checking (or something
> else)
> to some code. Where does your code come from in the first place?

I think I understand it. Some people would like to apply types with their hand,
and the others wouldn't like to do it. So, we are the former.

And, can't we imagine the middle way of them? That is:

* Library is designed with strong dependent types.
* Application and Middleware are designed with Higher-Order Model Checking.

Of course, that should be simply called by "type inference".
However, today's ATS2 type inference can't decide types correctly
(e.g. type of conditional expression in "If".)

How about adding Higher-Order model checking into ATS2 type inference?
In the past, most challenges are using general-purpose solver on this domain.
I think that Higher-Order model checking understands static contexts as
tree-ed type.

[Hongwei Xi]

>>Of course, that should be simply called by "type inference".
However, today's ATS2 type inference can't decide types correctly
(e.g. type of conditional expression in "If".)

Well, there is a reason for it. Say you have:

if (x > 0) then 1 else 2

What should be the type for this if-expression?

Assume that x has the type int(x). Then one type for the if-expression

is [i:int | (x > 0) && i==1 || not(x > 0) && i==2] int(i).

As you can see, this is a bit complex. Without type annotation, type inference
needs to infer most general types. You have to imagine how difficult it can be

to locate/fix type-errors in this way.

The purpose of type-checking is to find type-errors. If it takes (much) more time

for a programmer to go through type-error messages (reported by a type inference
algorithm) than for him/her to use type-annotations, then why should the programmer

refrain from using type-annotations?

>>the others wouldn't like to do it

Certainly. But this is no reason to think that these people would prefer to go through
error messages reported by a higher-order model-checker. These people may prefer

run-time debugging, for instance.

--
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 ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dnz6TC4HjNd39rRephHAGmb_oT01ePZNqtggqYwtseXXA%40mail.gmail.com.

[Kiwamu Okabe]

Hi Hongwei,

On Fri, Jan 9, 2015 at 5:13 AM, Hongwei Xi <gmh...@gmail.com> wrote:
> Well, there is a reason for it. Say you have:
>
> if (x > 0) then 1 else 2
>
> What should be the type for this if-expression?
>
> Assume that x has the type int(x). Then one type for the if-expression
> is [i:int | (x > 0) && i==1 || not(x > 0) && i==2] int(i).
>
> As you can see, this is a bit complex. Without type annotation, type
> inference
> needs to infer most general types. You have to imagine how difficult it can
> be
> to locate/fix type-errors in this way.

Do you mean that the types inferred full-automatically are hard to be fixed by
programmers, because they are very complex?

Umm... in conclusion, we doesn't have any solution to avoid "if test then"
idiom on ATS2?

Thank's for your time,

[Hongwei Xi]

What do you mean by "if test then" idiom?

--
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 ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dkeJsYzoWOPrpLpa3K%3DWtUvzpuFkuF-%3DhfzrL-WTUN_Gw%40mail.gmail.com.

[Kiwamu Okabe]

Hi Hongwei,

On Fri, Jan 9, 2015 at 3:47 PM, Hongwei Xi <gmh...@gmail.com> wrote:
> What do you mean by "if test then" idiom?

I think there are many such idiom on ATS2 source code.

(* File: prelude/DATS/CODEGEN/list_vt.atxt *)
case+ xs of
| @list_vt_cons
(x, xs1) => let
val test =
list_vt_filterlin$pred<a> (x)
in
if test then let
val () = loop (xs1)
in

I would like to write following:

if (list_vt_filterlin$pred<a> (x)) then let
val () = loop (xs1)

Thank's,

[Hongwei Xi]

>>I would like to write following:

    if (list_vt_filterlin$pred<a> (x)) then let
      val () = loop (xs1)

What would happen if you do?

--
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 ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dk94f27mvcm12CBF6aYyvfMzZbbqAo8F1CQ9tOvQMHNmw%40mail.gmail.com.

[Kiwamu Okabe]

Hi Hongwei,

On Fri, Jan 9, 2015 at 3:59 PM, Hongwei Xi <gmh...@gmail.com> wrote:
>>>I would like to write following:
>
> if (list_vt_filterlin$pred<a> (x)) then let
> val () = loop (xs1)
>
> What would happen if you do?

Sometimes, I find a compile error.

[Kiwamu Okabe]

Hi Hongwei,

On Fri, Jan 9, 2015 at 4:01 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote:
> On Fri, Jan 9, 2015 at 3:59 PM, Hongwei Xi <gmh...@gmail.com> wrote:
>>>>I would like to write following:
>>
>> if (list_vt_filterlin$pred<a> (x)) then let
>> val () = loop (xs1)
>>
>> What would happen if you do?
>
> Sometimes, I find a compile error.

O.K.
I think I should report it, next time.
Nowadays, I haven't found it.

Thank's,

[Hongwei Xi]

I myself tend to write code in the so-called A-normal form.

This practice makes it very easy to insert debugging code

if needed. For instance,

let

   val test = ...

   val () = println! ("test = ", test)

in

  if test then ...

end

My "philosophy" is that if one is well-prepared for debugging, then one spends less on debugging.

It is a bit zen-like :)

--
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 ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dmOotH1SKhLA8L1vVn_W0pS15tcGhXxWivOZq60%3DTZqWg%40mail.gmail.com.