Dependent type is hard

Google Group
1

hi,
I am still trying to implement my parser combinator and I have big troubles
with dependent types because some structures are mutated and some closures
are reused.
Code is at :
http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=avXpjG91

Basically in this sample, the count_dvt acts like a stream and can be
modified when some data consumed. (follows this pattern
: https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATS-QA-LIST/qa-list-2015-01-03-2.dats)

And action_vt acts like a combinator. It defines some actions to be done on
count_dvt.

What is hard is I want action_vt to be used any number of times and
count_dvt to be mutable at any point.

Any advices to make it works ?

2

Hello Cyrille,

hi,
I am still trying to implement my parser combinator and I have big
troubles with dependent types because some structures are mutated and some
closures are reused.
Code is at :
http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=avXpjG91
http://www.google.com/url?q=http%3A%2F%2Fwww.ats-lang.org%2FSERVER%2FMYCODE%2FPatsoptaas_serve.php%3Fmycode_url%3Dhttp%3A%2F%2Fpastebin.com%2Fraw.php%3Fi%3DavXpjG91&sa=D&sntz=1&usg=AFQjCNHSco7SiAo2MGLGd2qwXit8kq0H0w

Basically in this sample, the count_dvt acts like a stream and can be
modified when some data consumed. (follows this pattern :
https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATS-QA-LIST/qa-list-2015-01-03-2.dats
)

And action_vt acts like a combinator. It defines some actions to be done
on count_dvt.

Why are you using indexed datatypes here? Could you drop the indices? I
guess you’ve extracted the code from a larger program where the indices
were necessary for something.

Here’s the same thing sans indexes:
http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=3Sr2W1qk

What is hard is I want action_vt to be used any number of times and
count_dvt to be mutable at any point.

You could implement a function for explicitly duplicating/sharing the
linear value:

extern
fun dup_count_vt (count: !count_dvt): count_dvt

And use it any time you want to get one more reference to the data
structure.

Internally, such a function would either do a deep copy of the passed in
argument (no refcounting is needed in this case), or it would bump the
refcount (if refcounting is used). Note that in the former case, mutation
doesn’t “propagate” to the copies (which is probably not what you want).

Hope this helps.

3

I took a quick look.

The style you use is the standard functional style.

Once you are done, you could try something along the following line.

In ATS, a simpler and more efficient way is to use the following type
for a parser:

typedef parser (t(token), a(ast)) = (&pstate(t) >> _) - a

where pstate is for the current state of parsing. You could imagine that
pstate contains the input and also information for reporting error messages.
In the case of a parsing failure, an exception is raised. I have an
unfinished
project following what is outlined above:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/contrib/libats-/hwxi/parcomb

If you do not like exceptions, then use

typedef parser (t(token), a(ast)) = (&pstate(t) >> _) -
Option_vt(a)

So a parser is very much like a state monad.

Later, we could have linear parsers:

datatype
parser(a, t) = PARSER(int(ref-count), &pstate(t) >> _) - a)

This makes it fairly straightforward to free parsers constructed during
parsing.

An example of reference counting can be found in the Locking and Unlocking
section
at the bottom of the ATS Intro book:

http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/INT2PROGINATS-BOOK.htmlOn Saturday, January 17, 2015 at 12:08:59 PM UTC-5, Cyrille Duret wrote:

I see how long is the path to ATS enlightenment :slight_smile:

My first attempt to define a simple parser combinator without any
dependent nor linear feature : #include "share/atspre_staload.hats"#include "share/HATS/atspre_staload_libats - Pastebin.com

By now I just defined string and seq combinators.
I will add some useful ones such as regex (using pcre), many, any, etc…

One can compile it with :
$ curl “http://pastebin.com/raw.php?i=vBbDFxzJ” > test_parser_ML.dats
$ patscc -DATS_MEMALLOC_GCBDW -o test_parser_ML test_parser_ML.dats -lgc
-latslib

My inspiration are both from C++ and javascript world :

I understand now it is better to create the “ML” version first, then
modify it progressively to add linear types and dependent types step by
step.

My question is : can we mix some code using garbage collection and linear
type in the same program ?
In that case what would be the compilation command line ?

Le jeudi 15 janvier 2015 20:58:34 UTC+1, gmhwxi a écrit :

Well, I think this is a bit like playing a music instrument.
Practice is needed. Before one could play, say, Chopin, one needs to try
playing a lot of simpler pieces :slight_smile:

There is no “magic” in typechecking in ATS. To use advanced features
in ATS effectively, one really needs to know how a program is
typechecked.

On Wednesday, January 14, 2015 at 11:08:39 AM UTC-5, Cyrille Duret wrote:

thanks Artyom,
I see dependent types can be really hard with imperative code.

Le mardi 13 janvier 2015 10:29:30 UTC+1, Artyom Shalkhakov a écrit :

Hello Cyrille,

On Monday, January 12, 2015 at 11:41:15 PM UTC+6, Cyrille Duret wrote:

hi,
I am still trying to implement my parser combinator and I have big
troubles with dependent types because some structures are mutated and some
closures are reused.
Code is at :
http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=avXpjG91
http://www.google.com/url?q=http%3A%2F%2Fwww.ats-lang.org%2FSERVER%2FMYCODE%2FPatsoptaas_serve.php%3Fmycode_url%3Dhttp%3A%2F%2Fpastebin.com%2Fraw.php%3Fi%3DavXpjG91&sa=D&sntz=1&usg=AFQjCNHSco7SiAo2MGLGd2qwXit8kq0H0w

Basically in this sample, the count_dvt acts like a stream and can be
modified when some data consumed. (follows this pattern :
https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATS-QA-LIST/qa-list-2015-01-03-2.dats
)

And action_vt acts like a combinator. It defines some actions to be
done on count_dvt.

Why are you using indexed datatypes here? Could you drop the indices? I
guess you’ve extracted the code from a larger program where the indices
were necessary for something.

Here’s the same thing sans indexes:
http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=3Sr2W1qk

What is hard is I want action_vt to be used any number of times and
count_dvt to be mutable at any point.

You could implement a function for explicitly duplicating/sharing the
linear value:

extern
fun dup_count_vt (count: !count_dvt): count_dvt

And use it any time you want to get one more reference to the data
structure.

Internally, such a function would either do a deep copy of the passed
in argument (no refcounting is needed in this case), or it would bump the
refcount (if refcounting is used). Note that in the former case, mutation
doesn’t “propagate” to the copies (which is probably not what you want).

Hope this helps.

Any advices to make it works ?

4

Implementing a linear version of parsing combinators can be challenging.
It may make sense if you try to do a non-linear version in ATS first.

Due to the need for backtracking, tokens need to be saved into a buffers
so that they may be used later. For unlimited backtracking, all the tokens
need to be saved. So one may simply read all the tokens into an array
(you can use libats/dynarray for this) before parsing.

To have linear parsers, you are likely in need of reference counting:

because parsers may be shared in the construction of other parsers.

So it is somewhat involved. I have yet to see a package of linear parsing
combinators.
If there is already one, then it is probably done in C++.On Monday, January 12, 2015 at 12:41:15 PM UTC-5, Cyrille Duret wrote:

hi,
I am still trying to implement my parser combinator and I have big
troubles with dependent types because some structures are mutated and some
closures are reused.
Code is at :
http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=avXpjG91

Basically in this sample, the count_dvt acts like a stream and can be
modified when some data consumed. (follows this pattern :
https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATS-QA-LIST/qa-list-2015-01-03-2.dats
)

And action_vt acts like a combinator. It defines some actions to be done
on count_dvt.

What is hard is I want action_vt to be used any number of times and
count_dvt to be mutable at any point.

Any advices to make it works ?

5

I see how long is the path to ATS enlightenment :slight_smile:

My first attempt to define a simple parser combinator without any dependent
nor linear feature : #include "share/atspre_staload.hats"#include "share/HATS/atspre_staload_libats - Pastebin.com

By now I just defined string and seq combinators.
I will add some useful ones such as regex (using pcre), many, any, etc…

One can compile it with :
$ curl “http://pastebin.com/raw.php?i=vBbDFxzJ” > test_parser_ML.dats
$ patscc -DATS_MEMALLOC_GCBDW -o test_parser_ML test_parser_ML.dats -lgc
-latslib

My inspiration are both from C++ and javascript world :

I understand now it is better to create the “ML” version first, then modify
it progressively to add linear types and dependent types step by step.

My question is : can we mix some code using garbage collection and linear
type in the same program ?
In that case what would be the compilation command line ?Le jeudi 15 janvier 2015 20:58:34 UTC+1, gmhwxi a écrit :

Well, I think this is a bit like playing a music instrument.
Practice is needed. Before one could play, say, Chopin, one needs to try
playing a lot of simpler pieces :slight_smile:

There is no “magic” in typechecking in ATS. To use advanced features
in ATS effectively, one really needs to know how a program is
typechecked.

On Wednesday, January 14, 2015 at 11:08:39 AM UTC-5, Cyrille Duret wrote:

thanks Artyom,
I see dependent types can be really hard with imperative code.

Le mardi 13 janvier 2015 10:29:30 UTC+1, Artyom Shalkhakov a écrit :

Hello Cyrille,

On Monday, January 12, 2015 at 11:41:15 PM UTC+6, Cyrille Duret wrote:

hi,
I am still trying to implement my parser combinator and I have big
troubles with dependent types because some structures are mutated and some
closures are reused.
Code is at :
http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=avXpjG91
http://www.google.com/url?q=http%3A%2F%2Fwww.ats-lang.org%2FSERVER%2FMYCODE%2FPatsoptaas_serve.php%3Fmycode_url%3Dhttp%3A%2F%2Fpastebin.com%2Fraw.php%3Fi%3DavXpjG91&sa=D&sntz=1&usg=AFQjCNHSco7SiAo2MGLGd2qwXit8kq0H0w

Basically in this sample, the count_dvt acts like a stream and can be
modified when some data consumed. (follows this pattern :
https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATS-QA-LIST/qa-list-2015-01-03-2.dats
)

And action_vt acts like a combinator. It defines some actions to be
done on count_dvt.

Why are you using indexed datatypes here? Could you drop the indices? I
guess you’ve extracted the code from a larger program where the indices
were necessary for something.

Here’s the same thing sans indexes:
http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=3Sr2W1qk

What is hard is I want action_vt to be used any number of times and
count_dvt to be mutable at any point.

You could implement a function for explicitly duplicating/sharing the
linear value:

extern
fun dup_count_vt (count: !count_dvt): count_dvt

And use it any time you want to get one more reference to the data
structure.

Internally, such a function would either do a deep copy of the passed in
argument (no refcounting is needed in this case), or it would bump the
refcount (if refcounting is used). Note that in the former case, mutation
doesn’t “propagate” to the copies (which is probably not what you want).

Hope this helps.

Any advices to make it works ?

6

Well, I think this is a bit like playing a music instrument.
Practice is needed. Before one could play, say, Chopin, one needs to try
playing a lot of simpler pieces :slight_smile:

There is no “magic” in typechecking in ATS. To use advanced features
in ATS effectively, one really needs to know how a program is typechecked.On Wednesday, January 14, 2015 at 11:08:39 AM UTC-5, Cyrille Duret wrote:

thanks Artyom,
I see dependent types can be really hard with imperative code.

Le mardi 13 janvier 2015 10:29:30 UTC+1, Artyom Shalkhakov a écrit :

Hello Cyrille,

On Monday, January 12, 2015 at 11:41:15 PM UTC+6, Cyrille Duret wrote:

hi,
I am still trying to implement my parser combinator and I have big
troubles with dependent types because some structures are mutated and some
closures are reused.
Code is at :
http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=avXpjG91
http://www.google.com/url?q=http%3A%2F%2Fwww.ats-lang.org%2FSERVER%2FMYCODE%2FPatsoptaas_serve.php%3Fmycode_url%3Dhttp%3A%2F%2Fpastebin.com%2Fraw.php%3Fi%3DavXpjG91&sa=D&sntz=1&usg=AFQjCNHSco7SiAo2MGLGd2qwXit8kq0H0w

Basically in this sample, the count_dvt acts like a stream and can be
modified when some data consumed. (follows this pattern :
https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATS-QA-LIST/qa-list-2015-01-03-2.dats
)

And action_vt acts like a combinator. It defines some actions to be done
on count_dvt.

Why are you using indexed datatypes here? Could you drop the indices? I
guess you’ve extracted the code from a larger program where the indices
were necessary for something.

Here’s the same thing sans indexes:
http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=3Sr2W1qk

What is hard is I want action_vt to be used any number of times and
count_dvt to be mutable at any point.

You could implement a function for explicitly duplicating/sharing the
linear value:

extern
fun dup_count_vt (count: !count_dvt): count_dvt

And use it any time you want to get one more reference to the data
structure.

Internally, such a function would either do a deep copy of the passed in
argument (no refcounting is needed in this case), or it would bump the
refcount (if refcounting is used). Note that in the former case, mutation
doesn’t “propagate” to the copies (which is probably not what you want).

Hope this helps.

Any advices to make it works ?

7

thanks Artyom,
I see dependent types can be really hard with imperative code.Le mardi 13 janvier 2015 10:29:30 UTC+1, Artyom Shalkhakov a écrit :

Hello Cyrille,

On Monday, January 12, 2015 at 11:41:15 PM UTC+6, Cyrille Duret wrote:

hi,
I am still trying to implement my parser combinator and I have big
troubles with dependent types because some structures are mutated and some
closures are reused.
Code is at :
http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=avXpjG91
http://www.google.com/url?q=http%3A%2F%2Fwww.ats-lang.org%2FSERVER%2FMYCODE%2FPatsoptaas_serve.php%3Fmycode_url%3Dhttp%3A%2F%2Fpastebin.com%2Fraw.php%3Fi%3DavXpjG91&sa=D&sntz=1&usg=AFQjCNHSco7SiAo2MGLGd2qwXit8kq0H0w

Basically in this sample, the count_dvt acts like a stream and can be
modified when some data consumed. (follows this pattern :
https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATS-QA-LIST/qa-list-2015-01-03-2.dats
)

And action_vt acts like a combinator. It defines some actions to be done
on count_dvt.

Why are you using indexed datatypes here? Could you drop the indices? I
guess you’ve extracted the code from a larger program where the indices
were necessary for something.

Here’s the same thing sans indexes:
http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=3Sr2W1qk

What is hard is I want action_vt to be used any number of times and
count_dvt to be mutable at any point.

You could implement a function for explicitly duplicating/sharing the
linear value:

extern
fun dup_count_vt (count: !count_dvt): count_dvt

And use it any time you want to get one more reference to the data
structure.

Internally, such a function would either do a deep copy of the passed in
argument (no refcounting is needed in this case), or it would bump the
refcount (if refcounting is used). Note that in the former case, mutation
doesn’t “propagate” to the copies (which is probably not what you want).

Hope this helps.

Any advices to make it works ?

8

My question is : can we mix some code using garbage collection and linear
type in the same program?

Yes. I myself do this all the time. A programmer can often tell which part
of his or her program is a bottleneck
in terms of memory usage. Using linear types can be a very effective way to
address this kind of bottleneck issue.
For instance, I used linear types in my implementation of the
constraint-solving for ATS. Also, the part for testing
whether pattern matching is exhaustive was first done using non-linear
types; due to heavy GC, one often experienced
pause during compilation. Using linear type to re-implement this part
improved the performance very significantly.

In that case what would be the compilation command line?

You can add -DATS_MEMALLOC_GCBDW and -lgc. This means that malloc/free is
handled my libgc (Boehm-GC).On Saturday, January 17, 2015 at 12:08:59 PM UTC-5, Cyrille Duret wrote:

I see how long is the path to ATS enlightenment :slight_smile:

My first attempt to define a simple parser combinator without any
dependent nor linear feature : #include "share/atspre_staload.hats"#include "share/HATS/atspre_staload_libats - Pastebin.com

By now I just defined string and seq combinators.
I will add some useful ones such as regex (using pcre), many, any, etc…

One can compile it with :
$ curl “http://pastebin.com/raw.php?i=vBbDFxzJ” > test_parser_ML.dats
$ patscc -DATS_MEMALLOC_GCBDW -o test_parser_ML test_parser_ML.dats -lgc
-latslib

My inspiration are both from C++ and javascript world :

I understand now it is better to create the “ML” version first, then
modify it progressively to add linear types and dependent types step by
step.

My question is : can we mix some code using garbage collection and linear
type in the same program ?
In that case what would be the compilation command line ?

Le jeudi 15 janvier 2015 20:58:34 UTC+1, gmhwxi a écrit :

Well, I think this is a bit like playing a music instrument.
Practice is needed. Before one could play, say, Chopin, one needs to try
playing a lot of simpler pieces :slight_smile:

There is no “magic” in typechecking in ATS. To use advanced features
in ATS effectively, one really needs to know how a program is
typechecked.

On Wednesday, January 14, 2015 at 11:08:39 AM UTC-5, Cyrille Duret wrote:

thanks Artyom,
I see dependent types can be really hard with imperative code.

Le mardi 13 janvier 2015 10:29:30 UTC+1, Artyom Shalkhakov a écrit :

Hello Cyrille,

On Monday, January 12, 2015 at 11:41:15 PM UTC+6, Cyrille Duret wrote:

hi,
I am still trying to implement my parser combinator and I have big
troubles with dependent types because some structures are mutated and some
closures are reused.
Code is at :
http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=avXpjG91
http://www.google.com/url?q=http%3A%2F%2Fwww.ats-lang.org%2FSERVER%2FMYCODE%2FPatsoptaas_serve.php%3Fmycode_url%3Dhttp%3A%2F%2Fpastebin.com%2Fraw.php%3Fi%3DavXpjG91&sa=D&sntz=1&usg=AFQjCNHSco7SiAo2MGLGd2qwXit8kq0H0w

Basically in this sample, the count_dvt acts like a stream and can be
modified when some data consumed. (follows this pattern :
https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATS-QA-LIST/qa-list-2015-01-03-2.dats
)

And action_vt acts like a combinator. It defines some actions to be
done on count_dvt.

Why are you using indexed datatypes here? Could you drop the indices? I
guess you’ve extracted the code from a larger program where the indices
were necessary for something.

Here’s the same thing sans indexes:
http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=3Sr2W1qk

What is hard is I want action_vt to be used any number of times and
count_dvt to be mutable at any point.

You could implement a function for explicitly duplicating/sharing the
linear value:

extern
fun dup_count_vt (count: !count_dvt): count_dvt

And use it any time you want to get one more reference to the data
structure.

Internally, such a function would either do a deep copy of the passed
in argument (no refcounting is needed in this case), or it would bump the
refcount (if refcounting is used). Note that in the former case, mutation
doesn’t “propagate” to the copies (which is probably not what you want).

Hope this helps.

Any advices to make it works ?

9

What I see here is something I call the complexity trap of dependent types.
One can so easily get into unmanageable complexity when using dependent
types.

In general, please think of dependent types as a form of refinement. You
start out without dependent types. You add dependent types later to do
so-called
static debugging. The same can also be said about linear types.

In your case, I think the abstract type ‘count’ should be non-dependent:

absvtype count_vtype
vtypedef count = count_vtype

When you implement ‘count’, you could use a dependent version.

Similarly, ‘action’ should probably be non-dependent as well:

absvtype action_vtype
vtypedef action = action_vtype

It is not yet clear to me at this point how ‘action’ is supposed to be used.On Monday, January 12, 2015 at 12:41:15 PM UTC-5, Cyrille Duret wrote:

hi,
I am still trying to implement my parser combinator and I have big
troubles with dependent types because some structures are mutated and some
closures are reused.
Code is at :
http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=http://pastebin.com/raw.php?i=avXpjG91

Basically in this sample, the count_dvt acts like a stream and can be
modified when some data consumed. (follows this pattern :
https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATS-QA-LIST/qa-list-2015-01-03-2.dats
)

And action_vt acts like a combinator. It defines some actions to be done
on count_dvt.

What is hard is I want action_vt to be used any number of times and
count_dvt to be mutable at any point.

Any advices to make it works ?