Disagreements with the typechecker

Google Group
1

Continuing down the rabbit hole of type errors, I have a function to
tell me if a character in a string needs to be escaped, and how to do
it:

fun escape {c:int8} (c : char c) : [rc:int8 | rc != 0] @(bool, char rc) =
  case c of
  | '\n' => @(true, 'n')
  (* more cases snipped *)
  | '\0' => @(true, '0')
  | _    => @(false, c)

Now, patsopt chokes on this with

error(3): unsolved constraint: C3NSTRprop(main; S2Eapp(S2Ecst(!=); S2EVar(4098->S2Evar(c(7574))), S2Eintinf(0)))

which I’ve decoded to

error(3): unsolved constraint: c != 0

Which looks like ATS sees the path through _ returning c, and is
trying to show that c satisfies the constraints that rc has, which
doesn’t work. Yet, I believe I’ve handed the case of c == '\0', so I
would expect it to see that if we put 0 in, then rc == char '0', and
thus the constraint is satisfied. I’m assuming that I’ve hit a case
where what I’ve done is safe, but the type checker can’t understand why.

(To preemptively answer a likely question, [rc:int8 | rc != 0] is
needed because strnptr_set_at_gint takes a charNZ which is typed
similarly.)

So, is there either (a) a way to overrule the type checker and say “No! I
assure that this code is typed correctly!”, or (b) a way to structure
this function such that the type checker will understand its correctness?

(Surprisingly, doing _ => ( assertloc (c != 0) ; @(false, c) ) doesn’t
fix the issue?)

And as I’m still working on the previous question I asked, I’ll add
here that $showtype is exceedingly useful for trying to understand
typing issues. I don’t see it publicly documented anywhere, so might I
suggest doing so?

2

If you don’t mind having a runtime check, this one is good, too:

fun
escape{c:int8}
(
c : char c
) : [rc:int8 | rc != 0] @(bool, char rc) =
case c of
| ‘\n’ => @(true, ‘n’)
(* more cases snipped *)
| ‘\0’ => @(true, ‘0’)
| _ => let val () = assertloc (c != ‘\0’) in @(false, c) endOn Monday, August 4, 2014 8:41:49 PM UTC-4, gmhwxi wrote:

Unfortunately, pattern matching does not handle dependent char type
right now.

Here is a version that works:

fun
escape
{c:int8} (
c : char c
) : [rc:int8 | rc != 0] @(bool, char rc) =
if c = ‘\n’
then @(true, ‘n’)
else if c = ‘\0’
then @(true, ‘0’)
else @(false, c)

On Monday, August 4, 2014 8:14:39 PM UTC-4, Alex Miller wrote:

Continuing down the rabbit hole of type errors, I have a function to
tell me if a character in a string needs to be escaped, and how to do
it:

fun escape {c:int8} (c : char c) : [rc:int8 | rc != 0] @(bool, char

rc) =
case c of
| ‘\n’ => @(true, ‘n’)
(* more cases snipped *)
| ‘\0’ => @(true, ‘0’)
| _ => @(false, c)

Now, patsopt chokes on this with

error(3): unsolved constraint: C3NSTRprop(main; S2Eapp(S2Ecst(!=);

S2EVar(4098->S2Evar(c(7574))), S2Eintinf(0)))

which I’ve decoded to

error(3): unsolved constraint: c != 0

Which looks like ATS sees the path through _ returning c, and is
trying to show that c satisfies the constraints that rc has, which
doesn’t work. Yet, I believe I’ve handed the case of c == '\0', so I
would expect it to see that if we put 0 in, then rc == char '0', and
thus the constraint is satisfied. I’m assuming that I’ve hit a case
where what I’ve done is safe, but the type checker can’t understand why.

(To preemptively answer a likely question, [rc:int8 | rc != 0] is
needed because strnptr_set_at_gint takes a charNZ which is typed
similarly.)

So, is there either (a) a way to overrule the type checker and say “No! I
assure that this code is typed correctly!”, or (b) a way to structure
this function such that the type checker will understand its correctness?

(Surprisingly, doing _ => ( assertloc (c != 0) ; @(false, c) ) doesn’t
fix the issue?)

And as I’m still working on the previous question I asked, I’ll add
here that $showtype is exceedingly useful for trying to understand
typing issues. I don’t see it publicly documented anywhere, so might I
suggest doing so?

3

The following macros are defined in ${PATSHOME}/macrodef.dats

macdef showtype (x) = $showtype ,(x)
macdef showview (x) = pridentity ($showtype ,(x))

So you can write

val x = ref (0)
prval pf = showtype (x)

showview is for showing the view of a proof.

Btw, showview was given the name showlvaltype in the current release
(ATS2-0.1.1).On Tuesday, August 5, 2014 1:02:51 PM UTC-4, Brandon Barker wrote:

I agree that $showtype is a very helpful tool so I have put somewhat
prominently in the wiki here:

ats2-lang / Wiki / Error messages

(which I’d like to clarify more, see the rest of the e-mail)

and here:

ats2-lang / Wiki / Typechecking directives

By the way, I found that while learning ATS basics the wiki was a helpful
place to write things down to reference later and solidify my understanding
a bit more. I encourage other new users to do the same if possible.

I know some people don’t like the sf.net wiki, but it is all in markdown
and can be easily
migrated elsewhere (even if the elsewhere doesn’t use markdown) should
there be an impetus to do so.

On Monday, August 4, 2014 8:14:39 PM UTC-4, Alex Miller wrote:

Continuing down the rabbit hole of type errors, I have a function to
tell me if a character in a string needs to be escaped, and how to do
it:

fun escape {c:int8} (c : char c) : [rc:int8 | rc != 0] @(bool, char

rc) =
case c of
| ‘\n’ => @(true, ‘n’)
(* more cases snipped *)
| ‘\0’ => @(true, ‘0’)
| _ => @(false, c)

Now, patsopt chokes on this with

error(3): unsolved constraint: C3NSTRprop(main; S2Eapp(S2Ecst(!=);

S2EVar(4098->S2Evar(c(7574))), S2Eintinf(0)))

which I’ve decoded to

error(3): unsolved constraint: c != 0

Which looks like ATS sees the path through _ returning c, and is
trying to show that c satisfies the constraints that rc has, which
doesn’t work. Yet, I believe I’ve handed the case of c == '\0', so I
would expect it to see that if we put 0 in, then rc == char '0', and
thus the constraint is satisfied. I’m assuming that I’ve hit a case
where what I’ve done is safe, but the type checker can’t understand why.

(To preemptively answer a likely question, [rc:int8 | rc != 0] is
needed because strnptr_set_at_gint takes a charNZ which is typed
similarly.)

So, is there either (a) a way to overrule the type checker and say “No! I
assure that this code is typed correctly!”, or (b) a way to structure
this function such that the type checker will understand its correctness?

(Surprisingly, doing _ => ( assertloc (c != 0) ; @(false, c) ) doesn’t
fix the issue?)

And as I’m still working on the previous question I asked, I’ll add
here that $showtype is exceedingly useful for trying to understand
typing issues. I don’t see it publicly documented anywhere, so might I
suggest doing so?

4

To overrule the typechecker, you can do

staload UN = “prelude/SATS/unsafe.sats”

fun
escape{c:int8}
(
c : char c
) : [rc:int8 | rc != 0] @(bool, char rc) =
case c of
| ‘\n’ => @(true, ‘n’)
(* more cases snipped *)
| ‘\0’ => @(true, ‘0’)
| _ => let val c = $UN.cast{charNZ}(c) in @(false, c) endOn Monday, August 4, 2014 8:46:15 PM UTC-4, gmhwxi wrote:

If you don’t mind having a runtime check, this one is good, too:

fun
escape{c:int8}
(
c : char c
) : [rc:int8 | rc != 0] @(bool, char rc) =
case c of
| ‘\n’ => @(true, ‘n’)
(* more cases snipped *)
| ‘\0’ => @(true, ‘0’)
| _ => let val () = assertloc (c != ‘\0’) in @(false, c) end

On Monday, August 4, 2014 8:41:49 PM UTC-4, gmhwxi wrote:

Unfortunately, pattern matching does not handle dependent char type
right now.

Here is a version that works:

fun
escape
{c:int8} (
c : char c
) : [rc:int8 | rc != 0] @(bool, char rc) =
if c = ‘\n’
then @(true, ‘n’)
else if c = ‘\0’
then @(true, ‘0’)
else @(false, c)

On Monday, August 4, 2014 8:14:39 PM UTC-4, Alex Miller wrote:

Continuing down the rabbit hole of type errors, I have a function to
tell me if a character in a string needs to be escaped, and how to do
it:

fun escape {c:int8} (c : char c) : [rc:int8 | rc != 0] @(bool, char

rc) =
case c of
| ‘\n’ => @(true, ‘n’)
(* more cases snipped *)
| ‘\0’ => @(true, ‘0’)
| _ => @(false, c)

Now, patsopt chokes on this with

error(3): unsolved constraint: C3NSTRprop(main; S2Eapp(S2Ecst(!=);

S2EVar(4098->S2Evar(c(7574))), S2Eintinf(0)))

which I’ve decoded to

error(3): unsolved constraint: c != 0

Which looks like ATS sees the path through _ returning c, and is
trying to show that c satisfies the constraints that rc has, which
doesn’t work. Yet, I believe I’ve handed the case of c == '\0', so I
would expect it to see that if we put 0 in, then rc == char '0', and
thus the constraint is satisfied. I’m assuming that I’ve hit a case
where what I’ve done is safe, but the type checker can’t understand why.

(To preemptively answer a likely question, [rc:int8 | rc != 0] is
needed because strnptr_set_at_gint takes a charNZ which is typed
similarly.)

So, is there either (a) a way to overrule the type checker and say “No!
I
assure that this code is typed correctly!”, or (b) a way to structure
this function such that the type checker will understand its
correctness?

(Surprisingly, doing _ => ( assertloc (c != 0) ; @(false, c) ) doesn’t
fix the issue?)

And as I’m still working on the previous question I asked, I’ll add
here that $showtype is exceedingly useful for trying to understand
typing issues. I don’t see it publicly documented anywhere, so might I
suggest doing so?

5

Unfortunately, pattern matching does not handle dependent char type
right now.

(ignorant/clueless me) i wonder, from a usability standpoint, if there
might there be a way to signal that, to nip such wild goose chases in
the bud? or is it something that is a near-term todo? no skin the game
just wondering.

6

I have just implemented it. As integer patterns are already handled
properly, it is mostly straightforward to handle char patterns.

The changes are in the github-version of ATS2, and they will be available
in the next release.

However, I have to say that using asserts and $UN.cast is essential in
practice. One
simply cannot afford to wait in a situation like this until learning
necessary typing features.
Move on even if you have to use unsafe features …On Monday, August 4, 2014 8:44:31 PM UTC-4, Raoul Duke wrote:

Unfortunately, pattern matching does not handle dependent char type
right now.

(ignorant/clueless me) i wonder, from a usability standpoint, if there
might there be a way to signal that, to nip such wild goose chases in
the bud? or is it something that is a near-term todo? no skin the game
just wondering.

7

Unfortunately, pattern matching does not handle dependent char type
right now.

Here is a version that works:

fun
escape
{c:int8} (
c : char c
) : [rc:int8 | rc != 0] @(bool, char rc) =
if c = ‘\n’
then @(true, ‘n’)
else if c = ‘\0’
then @(true, ‘0’)
else @(false, c)On Monday, August 4, 2014 8:14:39 PM UTC-4, Alex Miller wrote:

Continuing down the rabbit hole of type errors, I have a function to
tell me if a character in a string needs to be escaped, and how to do
it:

fun escape {c:int8} (c : char c) : [rc:int8 | rc != 0] @(bool, char

rc) =
case c of
| ‘\n’ => @(true, ‘n’)
(* more cases snipped *)
| ‘\0’ => @(true, ‘0’)
| _ => @(false, c)

Now, patsopt chokes on this with

error(3): unsolved constraint: C3NSTRprop(main; S2Eapp(S2Ecst(!=);

S2EVar(4098->S2Evar(c(7574))), S2Eintinf(0)))

which I’ve decoded to

error(3): unsolved constraint: c != 0

Which looks like ATS sees the path through _ returning c, and is
trying to show that c satisfies the constraints that rc has, which
doesn’t work. Yet, I believe I’ve handed the case of c == '\0', so I
would expect it to see that if we put 0 in, then rc == char '0', and
thus the constraint is satisfied. I’m assuming that I’ve hit a case
where what I’ve done is safe, but the type checker can’t understand why.

(To preemptively answer a likely question, [rc:int8 | rc != 0] is
needed because strnptr_set_at_gint takes a charNZ which is typed
similarly.)

So, is there either (a) a way to overrule the type checker and say “No! I
assure that this code is typed correctly!”, or (b) a way to structure
this function such that the type checker will understand its correctness?

(Surprisingly, doing _ => ( assertloc (c != 0) ; @(false, c) ) doesn’t
fix the issue?)

And as I’m still working on the previous question I asked, I’ll add
here that $showtype is exceedingly useful for trying to understand
typing issues. I don’t see it publicly documented anywhere, so might I
suggest doing so?

8

Unfortunately, pattern matching does not handle dependent char type
right now.

Is this signified by

datatype
s2exp_node =
//…
(*
| S2Echar of char // chars have been removed for now
*)
//…

from pats_staexp2.sats, or if not could you give code pointers?

Here is a version that works:

fun
escape
{c:int8} (
c : char c
) : [rc:int8 | rc != 0] @(bool, char rc) =
if c = ‘\n’
then @(true, ‘n’)
else if c = ‘\0’
then @(true, ‘0’)
else @(false, c)

Ah, I should have thought to try chaining if/else as the poor man’s
switch statement. Thanks!> On Monday, August 4, 2014 8:14:39 PM UTC-4, Alex Miller wrote:

Continuing down the rabbit hole of type errors, I have a function to
tell me if a character in a string needs to be escaped, and how to do
it:

fun escape {c:int8} (c : char c) : [rc:int8 | rc != 0] @(bool, char

rc) =
case c of
| ‘\n’ => @(true, ‘n’)
(* more cases snipped *)
| ‘\0’ => @(true, ‘0’)
| _ => @(false, c)

Now, patsopt chokes on this with

error(3): unsolved constraint: C3NSTRprop(main; S2Eapp(S2Ecst(!=);

S2EVar(4098->S2Evar(c(7574))), S2Eintinf(0)))

which I’ve decoded to

error(3): unsolved constraint: c != 0

Which looks like ATS sees the path through _ returning c, and is
trying to show that c satisfies the constraints that rc has, which
doesn’t work. Yet, I believe I’ve handed the case of c == '\0', so I
would expect it to see that if we put 0 in, then rc == char '0', and
thus the constraint is satisfied. I’m assuming that I’ve hit a case
where what I’ve done is safe, but the type checker can’t understand why.

(To preemptively answer a likely question, [rc:int8 | rc != 0] is
needed because strnptr_set_at_gint takes a charNZ which is typed
similarly.)

So, is there either (a) a way to overrule the type checker and say “No! I
assure that this code is typed correctly!”, or (b) a way to structure
this function such that the type checker will understand its correctness?

(Surprisingly, doing _ => ( assertloc (c != 0) ; @(false, c) ) doesn’t
fix the issue?)

And as I’m still working on the previous question I asked, I’ll add
here that $showtype is exceedingly useful for trying to understand
typing issues. I don’t see it publicly documented anywhere, so might I
suggest doing so?

9

I agree that $showtype is a very helpful tool so I have put somewhat
prominently in the wiki here:

https://sourceforge.net/p/ats2-lang/wiki/Error%20messages/

(which I’d like to clarify more, see the rest of the e-mail)

and here:

https://sourceforge.net/p/ats2-lang/wiki/Typechecking%20directives/

By the way, I found that while learning ATS basics the wiki was a helpful
place to write things down to reference later and solidify my understanding
a bit more. I encourage other new users to do the same if possible.

I know some people don’t like the sf.net wiki, but it is all in markdown
and can be easily
migrated elsewhere (even if the elsewhere doesn’t use markdown) should
there be an impetus to do so.On Monday, August 4, 2014 8:14:39 PM UTC-4, Alex Miller wrote:

Continuing down the rabbit hole of type errors, I have a function to
tell me if a character in a string needs to be escaped, and how to do
it:

fun escape {c:int8} (c : char c) : [rc:int8 | rc != 0] @(bool, char

rc) =
case c of
| ‘\n’ => @(true, ‘n’)
(* more cases snipped *)
| ‘\0’ => @(true, ‘0’)
| _ => @(false, c)

Now, patsopt chokes on this with

error(3): unsolved constraint: C3NSTRprop(main; S2Eapp(S2Ecst(!=);

S2EVar(4098->S2Evar(c(7574))), S2Eintinf(0)))

which I’ve decoded to

error(3): unsolved constraint: c != 0

Which looks like ATS sees the path through _ returning c, and is
trying to show that c satisfies the constraints that rc has, which
doesn’t work. Yet, I believe I’ve handed the case of c == '\0', so I
would expect it to see that if we put 0 in, then rc == char '0', and
thus the constraint is satisfied. I’m assuming that I’ve hit a case
where what I’ve done is safe, but the type checker can’t understand why.

(To preemptively answer a likely question, [rc:int8 | rc != 0] is
needed because strnptr_set_at_gint takes a charNZ which is typed
similarly.)

So, is there either (a) a way to overrule the type checker and say “No! I
assure that this code is typed correctly!”, or (b) a way to structure
this function such that the type checker will understand its correctness?

(Surprisingly, doing _ => ( assertloc (c != 0) ; @(false, c) ) doesn’t
fix the issue?)

And as I’m still working on the previous question I asked, I’ll add
here that $showtype is exceedingly useful for trying to understand
typing issues. I don’t see it publicly documented anywhere, so might I
suggest doing so?

10

The code for handling this issue is actually inside pats_patcst2.dats.

Note that the last clause ‘_ => …’ needs to be changed into ‘_ =>> …’.

See:

http://www.ats-lang.org/DOCUMENT/INT2PROGINATS/HTML/x2772.htmlOn Monday, August 4, 2014 8:50:28 PM UTC-4, Alex Miller wrote:

On Aug 05 2014 at 00:41AM UTC, gmhwxi wrote:

Unfortunately, pattern matching does not handle dependent char type
right now.

Is this signified by

datatype
s2exp_node =
//…
(*
| S2Echar of char // chars have been removed for now
*)
//…

from pats_staexp2.sats, or if not could you give code pointers?

Here is a version that works:

fun
escape
{c:int8} (
c : char c
) : [rc:int8 | rc != 0] @(bool, char rc) =
if c = ‘\n’
then @(true, ‘n’)
else if c = ‘\0’
then @(true, ‘0’)
else @(false, c)

Ah, I should have thought to try chaining if/else as the poor man’s
switch statement. Thanks!

On Monday, August 4, 2014 8:14:39 PM UTC-4, Alex Miller wrote:

Continuing down the rabbit hole of type errors, I have a function to
tell me if a character in a string needs to be escaped, and how to do
it:

fun escape {c:int8} (c : char c) : [rc:int8 | rc != 0] @(bool,

char

rc) =
case c of
| ‘\n’ => @(true, ‘n’)
(* more cases snipped *)
| ‘\0’ => @(true, ‘0’)
| _ => @(false, c)

Now, patsopt chokes on this with

error(3): unsolved constraint: C3NSTRprop(main; S2Eapp(S2Ecst(!=);

S2EVar(4098->S2Evar(c(7574))), S2Eintinf(0)))

which I’ve decoded to

error(3): unsolved constraint: c != 0

Which looks like ATS sees the path through _ returning c, and is
trying to show that c satisfies the constraints that rc has, which
doesn’t work. Yet, I believe I’ve handed the case of c == '\0', so
I
would expect it to see that if we put 0 in, then rc == char '0',
and
thus the constraint is satisfied. I’m assuming that I’ve hit a case
where what I’ve done is safe, but the type checker can’t understand
why.

(To preemptively answer a likely question, [rc:int8 | rc != 0] is
needed because strnptr_set_at_gint takes a charNZ which is typed
similarly.)

So, is there either (a) a way to overrule the type checker and say
“No! I
assure that this code is typed correctly!”, or (b) a way to structure
this function such that the type checker will understand its
correctness?

(Surprisingly, doing _ => ( assertloc (c != 0) ; @(false, c) )
doesn’t
fix the issue?)

And as I’m still working on the previous question I asked, I’ll add
here that $showtype is exceedingly useful for trying to understand
typing issues. I don’t see it publicly documented anywhere, so might
I
suggest doing so?