Constructor pattern cannot be assigned the type

Google Group
1

I understand (but not completely how) dataviewtypes have changed in ATS2.
That aside, there are likely numerous errors here that I should not be
having if I remembered everything I learned in ATS1 being that the output
of patsopt reminds me of some of my worst C++ compiler errors involving
heavy use of template libraries :).

I will just show what I have for the first part:

.sats:
fun{a:t0p}
linset_union (xs1: set(INV(a)), xs2: set(INV(a))): List0_vt (a)

.dats:
implement{a}
linset_union
(xs1, xs2) = let
//
fun aux // non-tail-recursive
{n1,n2:nat} .<n1+n2>.
(
xs1: list (a, n1), xs2: list (a, n2)
) :<> List0_vt (a) = let // should be able to return e.g. listGte_vt(a, n3)
in // where n3 >= min(n1, n2)
//
case xs1 of
| list_vt_cons
(x1, xs11) =>

Highlighted part gives the error:
/home/brand_000/ATS-Postiats/libats/DATS/linset_listord.dats:
10284(line=534, offs=3) – 10311(line=535, offs=15): error(3): the
constructor pattern cannot be assigned the type
[S2Eapp(S2Ecst(list_t0ype_int_type); S2Evar(a(7153)), S2Evar(n1(7155)))].
/home/brand_000/ATS-Postiats/libats/DATS/linset_listord.dats:
10338(line=538, offs=5) – 10361(line=538, offs=28): error(3): the
constructor pattern cannot be assigned the type
[S2Eapp(S2Ecst(list_t0ype_int_type); S2Evar(a(7153)), S2Evar(n2(7156)))].

2

I’m still having some trouble getting used to linear datatypes in ATS2,
though it looks like it will be a bit more straightforward than in ATS1.
Here’s an attempt for list_union; trouble seems to occur around free@ -
something to do with making the unfolded dataviewtypes inaccessible, but
i’m not sure how to get around that.

One other thing I’m unsure about is what is going on with bindings like:

val xs11 = xs11

full code at:

(* ****** ****** *)
implement{a}
linset_union
(xs1, xs2) = let
//
viewtypedef res = List_vt (a)
fun loop
{n1,n2:nat} .<n1+n2>. (
xs1: list_vt (a, n1), xs2: list_vt (a, n2), res: &res? >> res
) :<!wrt,cloref> void =
case+ xs1 of
| @list_vt_cons (x1, xs11) => (
case+ xs2 of
| @list_vt_cons (x2, xs21) => let
val sgn = compare_elt_elt (x1, x2)
in
if sgn < 0 then let
//val () = $showtype(xs11)
//val xs11 = xs11 // What does this do?
//val () = $showtype(xs11)
prval () = fold@ {a} (xs2)
val () = loop (xs11, xs2, xs11)
prval () = fold@ {a} (xs1)
in
res := xs1
end else if sgn > 0 then let
//val xs21 = xs21
prval () = fold@ {a} (xs1)
val () = loop (xs1, xs21, xs21)
prval () = fold@ (xs2)
in
res := xs2
end else let // x1 = x2
//val xs11 = xs11
//val xs21 = xs21
val () = free@ {a}{0} (xs2)
val () = loop (xs11, xs21, xs21)
prval () = fold@ (xs1)
in
res := xs1
end // end of [if]
end // end of [list_vt_cons]
| ~list_vt_nil () => (fold@ (xs1); res := xs1)
) // end of [list_vt_cons]
| ~list_vt_nil () => (res := xs2)
// end of [loop]
var res: res // uninitialized
val () = loop (xs1, xs2, res)
in
resOn Monday, January 13, 2014 9:38:30 PM UTC-5, Brandon Barker wrote:

That’ll do it … typo (due to copy/paste from funset).

On Monday, January 13, 2014 12:22:01 AM UTC-5, gmhwxi wrote:

xs1 is given the type list(a) but the constructor list_vt_cons is used;
list_cons should be used instead.

On Sunday, January 12, 2014 11:18:57 PM UTC-5, Brandon Barker wrote:

I understand (but not completely how) dataviewtypes have changed in
ATS2. That aside, there are likely numerous errors here that I should not
be having if I remembered everything I learned in ATS1 being that the
output of patsopt reminds me of some of my worst C++ compiler errors
involving heavy use of template libraries :).

I will just show what I have for the first part:

.sats:
fun{a:t0p}
linset_union (xs1: set(INV(a)), xs2: set(INV(a))): List0_vt (a)

.dats:
implement{a}
linset_union
(xs1, xs2) = let
//
fun aux // non-tail-recursive
{n1,n2:nat} .<n1+n2>.
(
xs1: list (a, n1), xs2: list (a, n2)
) :<> List0_vt (a) = let // should be able to return e.g. listGte_vt(a,
n3)
in // where n3 >= min(n1, n2)
//
case xs1 of
| list_vt_cons
(x1, xs11) =>

Highlighted part gives the error:
/home/brand_000/ATS-Postiats/libats/DATS/linset_listord.dats:
10284(line=534, offs=3) – 10311(line=535, offs=15): error(3): the
constructor pattern cannot be assigned the type
[S2Eapp(S2Ecst(list_t0ype_int_type); S2Evar(a(7153)), S2Evar(n1(7155)))].
/home/brand_000/ATS-Postiats/libats/DATS/linset_listord.dats:
10338(line=538, offs=5) – 10361(line=538, offs=28): error(3): the
constructor pattern cannot be assigned the type
[S2Eapp(S2Ecst(list_t0ype_int_type); S2Evar(a(7153)), S2Evar(n2(7156)))].
3

That’ll do it … typo (due to copy/paste from funset).On Monday, January 13, 2014 12:22:01 AM UTC-5, gmhwxi wrote:

xs1 is given the type list(a) but the constructor list_vt_cons is used;
list_cons should be used instead.

On Sunday, January 12, 2014 11:18:57 PM UTC-5, Brandon Barker wrote:

I understand (but not completely how) dataviewtypes have changed in ATS2.
That aside, there are likely numerous errors here that I should not be
having if I remembered everything I learned in ATS1 being that the output
of patsopt reminds me of some of my worst C++ compiler errors involving
heavy use of template libraries :).

I will just show what I have for the first part:

.sats:
fun{a:t0p}
linset_union (xs1: set(INV(a)), xs2: set(INV(a))): List0_vt (a)

.dats:
implement{a}
linset_union
(xs1, xs2) = let
//
fun aux // non-tail-recursive
{n1,n2:nat} .<n1+n2>.
(
xs1: list (a, n1), xs2: list (a, n2)
) :<> List0_vt (a) = let // should be able to return e.g. listGte_vt(a,
n3)
in // where n3 >= min(n1, n2)
//
case xs1 of
| list_vt_cons
(x1, xs11) =>

Highlighted part gives the error:
/home/brand_000/ATS-Postiats/libats/DATS/linset_listord.dats:
10284(line=534, offs=3) – 10311(line=535, offs=15): error(3): the
constructor pattern cannot be assigned the type
[S2Eapp(S2Ecst(list_t0ype_int_type); S2Evar(a(7153)), S2Evar(n1(7155)))].
/home/brand_000/ATS-Postiats/libats/DATS/linset_listord.dats:
10338(line=538, offs=5) – 10361(line=538, offs=28): error(3): the
constructor pattern cannot be assigned the type
[S2Eapp(S2Ecst(list_t0ype_int_type); S2Evar(a(7153)), S2Evar(n2(7156)))].

4

See the following code:

case+ xs1 of
| @list_vt_cons (x1, xs11) => (
case+ xs2 of
| @list_vt_cons (x2, xs21) => let
val sgn = compare_elt_elt (x1, x2)
in
if sgn < 0 then let
val xs11_ = xs11
prval () = fold@ {a} (xs2)
val () = loop (xs11_, xs2, xs11)
prval () = fold@ {a} (xs1)
in
res := xs1
end else if sgn > 0 then let
val xs21_ = xs21
prval () = fold@ {a} (xs1)
val () = loop (xs1, xs21_, xs21)
prval () = fold@ (xs2)
in
res := xs2
end else let // x1 = x2
val xs11_ = xs11
val xs21_ = xs21
val () = free@ {a}{0} (xs2)
val () = loop (xs11_, xs21_, xs11)
prval () = fold@ (xs1)
in
res := xs1
end // end of [if]
end // end of [list_vt_cons]
| ~list_vt_nil () => (fold@ (xs1); res := xs1)
) // end of [list_vt_cons]
| ~list_vt_nil () => (res := xs2)On Thursday, January 16, 2014 12:02:44 PM UTC-5, Brandon Barker wrote:

left off an “end” at the end of the pasted implementation.

On Thursday, January 16, 2014 12:01:54 PM UTC-5, Brandon Barker wrote:

I’m still having some trouble getting used to linear datatypes in ATS2,
though it looks like it will be a bit more straightforward than in ATS1.
Here’s an attempt for list_union; trouble seems to occur around free@ -
something to do with making the unfolded dataviewtypes inaccessible, but
i’m not sure how to get around that.

One other thing I’m unsure about is what is going on with bindings like:

val xs11 = xs11

full code at:
Comparing githwxi:master...bbarker:master · githwxi/ATS-Postiats · GitHub

(* ****** ****** *)
implement{a}
linset_union
(xs1, xs2) = let
//
viewtypedef res = List_vt (a)
fun loop
{n1,n2:nat} .<n1+n2>. (
xs1: list_vt (a, n1), xs2: list_vt (a, n2), res: &res? >> res
) :<!wrt,cloref> void =
case+ xs1 of
| @list_vt_cons (x1, xs11) => (
case+ xs2 of
| @list_vt_cons (x2, xs21) => let
val sgn = compare_elt_elt (x1, x2)
in
if sgn < 0 then let
//val () = $showtype(xs11)
//val xs11 = xs11 // What does this do?
//val () = $showtype(xs11)
prval () = fold@ {a} (xs2)
val () = loop (xs11, xs2, xs11)
prval () = fold@ {a} (xs1)
in
res := xs1
end else if sgn > 0 then let
//val xs21 = xs21
prval () = fold@ {a} (xs1)
val () = loop (xs1, xs21, xs21)
prval () = fold@ (xs2)
in
res := xs2
end else let // x1 = x2
//val xs11 = xs11
//val xs21 = xs21
val () = free@ {a}{0} (xs2)
val () = loop (xs11, xs21, xs21)
prval () = fold@ (xs1)
in
res := xs1
end // end of [if]
end // end of [list_vt_cons]
| ~list_vt_nil () => (fold@ (xs1); res := xs1)
) // end of [list_vt_cons]
| ~list_vt_nil () => (res := xs2)
// end of [loop]
var res: res // uninitialized
val () = loop (xs1, xs2, res)
in
res

On Monday, January 13, 2014 9:38:30 PM UTC-5, Brandon Barker wrote:

That’ll do it … typo (due to copy/paste from funset).

On Monday, January 13, 2014 12:22:01 AM UTC-5, gmhwxi wrote:

xs1 is given the type list(a) but the constructor list_vt_cons is used;
list_cons should be used instead.

On Sunday, January 12, 2014 11:18:57 PM UTC-5, Brandon Barker wrote:

I understand (but not completely how) dataviewtypes have changed in
ATS2. That aside, there are likely numerous errors here that I should not
be having if I remembered everything I learned in ATS1 being that the
output of patsopt reminds me of some of my worst C++ compiler errors
involving heavy use of template libraries :).

I will just show what I have for the first part:

.sats:
fun{a:t0p}
linset_union (xs1: set(INV(a)), xs2: set(INV(a))): List0_vt (a)

.dats:
implement{a}
linset_union
(xs1, xs2) = let
//
fun aux // non-tail-recursive
{n1,n2:nat} .<n1+n2>.
(
xs1: list (a, n1), xs2: list (a, n2)
) :<> List0_vt (a) = let // should be able to return e.g.
listGte_vt(a, n3)
in // where n3 >= min(n1, n2)
//
case xs1 of
| list_vt_cons
(x1, xs11) =>

Highlighted part gives the error:
/home/brand_000/ATS-Postiats/libats/DATS/linset_listord.dats:
10284(line=534, offs=3) – 10311(line=535, offs=15): error(3): the
constructor pattern cannot be assigned the type
[S2Eapp(S2Ecst(list_t0ype_int_type); S2Evar(a(7153)), S2Evar(n1(7155)))].
/home/brand_000/ATS-Postiats/libats/DATS/linset_listord.dats:
10338(line=538, offs=5) – 10361(line=538, offs=28): error(3): the
constructor pattern cannot be assigned the type
[S2Eapp(S2Ecst(list_t0ype_int_type); S2Evar(a(7153)), S2Evar(n2(7156)))].

5

left off an “end” at the end of the pasted implementation.On Thursday, January 16, 2014 12:01:54 PM UTC-5, Brandon Barker wrote:

I’m still having some trouble getting used to linear datatypes in ATS2,
though it looks like it will be a bit more straightforward than in ATS1.
Here’s an attempt for list_union; trouble seems to occur around free@ -
something to do with making the unfolded dataviewtypes inaccessible, but
i’m not sure how to get around that.

One other thing I’m unsure about is what is going on with bindings like:

val xs11 = xs11

full code at:
Comparing githwxi:master...bbarker:master · githwxi/ATS-Postiats · GitHub

(* ****** ****** *)
implement{a}
linset_union
(xs1, xs2) = let
//
viewtypedef res = List_vt (a)
fun loop
{n1,n2:nat} .<n1+n2>. (
xs1: list_vt (a, n1), xs2: list_vt (a, n2), res: &res? >> res
) :<!wrt,cloref> void =
case+ xs1 of
| @list_vt_cons (x1, xs11) => (
case+ xs2 of
| @list_vt_cons (x2, xs21) => let
val sgn = compare_elt_elt (x1, x2)
in
if sgn < 0 then let
//val () = $showtype(xs11)
//val xs11 = xs11 // What does this do?
//val () = $showtype(xs11)
prval () = fold@ {a} (xs2)
val () = loop (xs11, xs2, xs11)
prval () = fold@ {a} (xs1)
in
res := xs1
end else if sgn > 0 then let
//val xs21 = xs21
prval () = fold@ {a} (xs1)
val () = loop (xs1, xs21, xs21)
prval () = fold@ (xs2)
in
res := xs2
end else let // x1 = x2
//val xs11 = xs11
//val xs21 = xs21
val () = free@ {a}{0} (xs2)
val () = loop (xs11, xs21, xs21)
prval () = fold@ (xs1)
in
res := xs1
end // end of [if]
end // end of [list_vt_cons]
| ~list_vt_nil () => (fold@ (xs1); res := xs1)
) // end of [list_vt_cons]
| ~list_vt_nil () => (res := xs2)
// end of [loop]
var res: res // uninitialized
val () = loop (xs1, xs2, res)
in
res

On Monday, January 13, 2014 9:38:30 PM UTC-5, Brandon Barker wrote:

That’ll do it … typo (due to copy/paste from funset).

On Monday, January 13, 2014 12:22:01 AM UTC-5, gmhwxi wrote:

xs1 is given the type list(a) but the constructor list_vt_cons is used;
list_cons should be used instead.

On Sunday, January 12, 2014 11:18:57 PM UTC-5, Brandon Barker wrote:

I understand (but not completely how) dataviewtypes have changed in
ATS2. That aside, there are likely numerous errors here that I should not
be having if I remembered everything I learned in ATS1 being that the
output of patsopt reminds me of some of my worst C++ compiler errors
involving heavy use of template libraries :).

I will just show what I have for the first part:

.sats:
fun{a:t0p}
linset_union (xs1: set(INV(a)), xs2: set(INV(a))): List0_vt (a)

.dats:
implement{a}
linset_union
(xs1, xs2) = let
//
fun aux // non-tail-recursive
{n1,n2:nat} .<n1+n2>.
(
xs1: list (a, n1), xs2: list (a, n2)
) :<> List0_vt (a) = let // should be able to return e.g.
listGte_vt(a, n3)
in // where n3 >= min(n1, n2)
//
case xs1 of
| list_vt_cons
(x1, xs11) =>

Highlighted part gives the error:
/home/brand_000/ATS-Postiats/libats/DATS/linset_listord.dats:
10284(line=534, offs=3) – 10311(line=535, offs=15): error(3): the
constructor pattern cannot be assigned the type
[S2Eapp(S2Ecst(list_t0ype_int_type); S2Evar(a(7153)), S2Evar(n1(7155)))].
/home/brand_000/ATS-Postiats/libats/DATS/linset_listord.dats:
10338(line=538, offs=5) – 10361(line=538, offs=28): error(3): the
constructor pattern cannot be assigned the type
[S2Eapp(S2Ecst(list_t0ype_int_type); S2Evar(a(7153)), S2Evar(n2(7156)))].

6

xs1 is given the type list(a) but the constructor list_vt_cons is used;
list_cons should be used instead.On Sunday, January 12, 2014 11:18:57 PM UTC-5, Brandon Barker wrote:

I understand (but not completely how) dataviewtypes have changed in ATS2.
That aside, there are likely numerous errors here that I should not be
having if I remembered everything I learned in ATS1 being that the output
of patsopt reminds me of some of my worst C++ compiler errors involving
heavy use of template libraries :).

I will just show what I have for the first part:

.sats:
fun{a:t0p}
linset_union (xs1: set(INV(a)), xs2: set(INV(a))): List0_vt (a)

.dats:
implement{a}
linset_union
(xs1, xs2) = let
//
fun aux // non-tail-recursive
{n1,n2:nat} .<n1+n2>.
(
xs1: list (a, n1), xs2: list (a, n2)
) :<> List0_vt (a) = let // should be able to return e.g. listGte_vt(a,
n3)
in // where n3 >= min(n1, n2)
//
case xs1 of
| list_vt_cons
(x1, xs11) =>

Highlighted part gives the error:
/home/brand_000/ATS-Postiats/libats/DATS/linset_listord.dats:
10284(line=534, offs=3) – 10311(line=535, offs=15): error(3): the
constructor pattern cannot be assigned the type
[S2Eapp(S2Ecst(list_t0ype_int_type); S2Evar(a(7153)), S2Evar(n1(7155)))].
/home/brand_000/ATS-Postiats/libats/DATS/linset_listord.dats:
10338(line=538, offs=5) – 10361(line=538, offs=28): error(3): the
constructor pattern cannot be assigned the type
[S2Eapp(S2Ecst(list_t0ype_int_type); S2Evar(a(7153)), S2Evar(n2(7156)))].

7

Thanks, I think I see: if RHS is a reference to a value of some viewtype,
val LHS = RHS

then LHS is the value of that viewtype itself. However, $showtype was not
very clear on this, but the type of xs11 did seem to change after the val
statement, but I wouldn’t that is correct.

$showtype(xs11) //says something about the viewtype (list_vt)
val xs11_ = xs11
$showtype(xs11_) //says something about the viewtype
$showtype(xs11) //also says something about the viewtype

I think in ATS1, we had to do:
val LHS = !RHS.On Thursday, January 16, 2014 5:16:33 PM UTC-5, gmhwxi wrote:

See the following code:

case+ xs1 of
| @list_vt_cons (x1, xs11) => (
case+ xs2 of
| @list_vt_cons (x2, xs21) => let
val sgn = compare_elt_elt (x1, x2)
in
if sgn < 0 then let
val xs11_ = xs11
prval () = fold@ {a} (xs2)
val () = loop (xs11_, xs2, xs11)
prval () = fold@ {a} (xs1)
in
res := xs1
end else if sgn > 0 then let
val xs21_ = xs21
prval () = fold@ {a} (xs1)
val () = loop (xs1, xs21_, xs21)
prval () = fold@ (xs2)
in
res := xs2
end else let // x1 = x2
val xs11_ = xs11
val xs21_ = xs21
val () = free@ {a}{0} (xs2)
val () = loop (xs11_, xs21_, xs11)
prval () = fold@ (xs1)
in
res := xs1
end // end of [if]
end // end of [list_vt_cons]
| ~list_vt_nil () => (fold@ (xs1); res := xs1)
) // end of [list_vt_cons]
| ~list_vt_nil () => (res := xs2)

On Thursday, January 16, 2014 12:02:44 PM UTC-5, Brandon Barker wrote:

left off an “end” at the end of the pasted implementation.

On Thursday, January 16, 2014 12:01:54 PM UTC-5, Brandon Barker wrote:

I’m still having some trouble getting used to linear datatypes in ATS2,
though it looks like it will be a bit more straightforward than in ATS1.
Here’s an attempt for list_union; trouble seems to occur around free@ -
something to do with making the unfolded dataviewtypes inaccessible, but
i’m not sure how to get around that.

One other thing I’m unsure about is what is going on with bindings like:

val xs11 = xs11

full code at:
Comparing githwxi:master...bbarker:master · githwxi/ATS-Postiats · GitHub

(* ****** ****** *)
implement{a}
linset_union
(xs1, xs2) = let
//
viewtypedef res = List_vt (a)
fun loop
{n1,n2:nat} .<n1+n2>. (
xs1: list_vt (a, n1), xs2: list_vt (a, n2), res: &res? >> res
) :<!wrt,cloref> void =
case+ xs1 of
| @list_vt_cons (x1, xs11) => (
case+ xs2 of
| @list_vt_cons (x2, xs21) => let
val sgn = compare_elt_elt (x1, x2)
in
if sgn < 0 then let
//val () = $showtype(xs11)
//val xs11 = xs11 // What does this do?
//val () = $showtype(xs11)
prval () = fold@ {a} (xs2)
val () = loop (xs11, xs2, xs11)
prval () = fold@ {a} (xs1)
in
res := xs1
end else if sgn > 0 then let
//val xs21 = xs21
prval () = fold@ {a} (xs1)
val () = loop (xs1, xs21, xs21)
prval () = fold@ (xs2)
in
res := xs2
end else let // x1 = x2
//val xs11 = xs11
//val xs21 = xs21
val () = free@ {a}{0} (xs2)
val () = loop (xs11, xs21, xs21)
prval () = fold@ (xs1)
in
res := xs1
end // end of [if]
end // end of [list_vt_cons]
| ~list_vt_nil () => (fold@ (xs1); res := xs1)
) // end of [list_vt_cons]
| ~list_vt_nil () => (res := xs2)
// end of [loop]
var res: res // uninitialized
val () = loop (xs1, xs2, res)
in
res

On Monday, January 13, 2014 9:38:30 PM UTC-5, Brandon Barker wrote:

That’ll do it … typo (due to copy/paste from funset).

On Monday, January 13, 2014 12:22:01 AM UTC-5, gmhwxi wrote:

xs1 is given the type list(a) but the constructor list_vt_cons is
used; list_cons should be used instead.

On Sunday, January 12, 2014 11:18:57 PM UTC-5, Brandon Barker wrote:

I understand (but not completely how) dataviewtypes have changed in
ATS2. That aside, there are likely numerous errors here that I should not
be having if I remembered everything I learned in ATS1 being that the
output of patsopt reminds me of some of my worst C++ compiler errors
involving heavy use of template libraries :).

I will just show what I have for the first part:

.sats:
fun{a:t0p}
linset_union (xs1: set(INV(a)), xs2: set(INV(a))): List0_vt (a)

.dats:
implement{a}
linset_union
(xs1, xs2) = let
//
fun aux // non-tail-recursive
{n1,n2:nat} .<n1+n2>.
(
xs1: list (a, n1), xs2: list (a, n2)
) :<> List0_vt (a) = let // should be able to return e.g.
listGte_vt(a, n3)
in // where n3 >= min(n1, n2)
//
case xs1 of
| list_vt_cons
(x1, xs11) =>

Highlighted part gives the error:
/home/brand_000/ATS-Postiats/libats/DATS/linset_listord.dats:
10284(line=534, offs=3) – 10311(line=535, offs=15): error(3): the
constructor pattern cannot be assigned the type
[S2Eapp(S2Ecst(list_t0ype_int_type); S2Evar(a(7153)), S2Evar(n1(7155)))].
/home/brand_000/ATS-Postiats/libats/DATS/linset_listord.dats:
10338(line=538, offs=5) – 10361(line=538, offs=28): error(3): the
constructor pattern cannot be assigned the type
[S2Eapp(S2Ecst(list_t0ype_int_type); S2Evar(a(7153)), S2Evar(n2(7156)))].