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

Google Group
1

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:

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.On Monday, January 5, 2015 2:43:31 AM UTC-5, Kiwamu Okabe wrote:

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

2

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 :slight_smile:

Are you familiar with liquid type (logically qualified types)?On Monday, January 5, 2015 9:07:58 PM UTC-5, gmhwxi wrote:

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.

On Monday, January 5, 2015 2:43:31 AM UTC-5, Kiwamu Okabe wrote:

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

3

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 :)On Fri, Jan 9, 2015 at 2:02 AM, Kiwamu Okabe kiw...@debian.or.jp wrote:

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,

Kiwamu Okabe at METASEPI DESIGN

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

4

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).On Tue, Jan 6, 2015 at 4:15 PM, Hongwei Xi gmh...@gmail.com wrote:

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

On Tue, Jan 6, 2015 at 2:41 AM, gmhwxi gmh...@gmail.com wrote:

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 :slight_smile:

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

On Monday, January 5, 2015 9:07:58 PM UTC-5, gmhwxi wrote:

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.

On Monday, January 5, 2015 2:43:31 AM UTC-5, Kiwamu Okabe wrote:

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

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
ats-lang-users List Signup and Options

–
Zhiqiang Ren

Department of Computer Science
Boston University

5

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.On Tue, Jan 6, 2015 at 2:41 AM, gmhwxi gmh...@gmail.com wrote:

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 :slight_smile:

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

On Monday, January 5, 2015 9:07:58 PM UTC-5, gmhwxi wrote:

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.

On Monday, January 5, 2015 2:43:31 AM UTC-5, Kiwamu Okabe wrote:

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

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
ats-lang-users List Signup and Options

Zhiqiang Ren

Department of Computer Science
Boston University

6

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.On Wed, Jan 7, 2015 at 11:49 PM, Kiwamu Okabe kiw...@debian.or.jp wrote:

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.

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

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

7

I would like to write following:

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

What would happen if you do?On Fri, Jan 9, 2015 at 1:52 AM, Kiwamu Okabe kiw...@debian.or.jp wrote:

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 (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,

Kiwamu Okabe at METASEPI DESIGN

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

8

What do you mean by “if test then” idiom?On Fri, Jan 9, 2015 at 1:35 AM, Kiwamu Okabe kiw...@debian.or.jp wrote:

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,

Kiwamu Okabe at METASEPI DESIGN

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