Constraining unspecified types

Google Group
1

The following is a minimal example of a typechecking issue I’ve been
chasing after for a while. I have an either type that I’ve implemented,
mimicing the standard library’s option type:

datatype either_t0ype_bool_type
  (a : t@ype+, b : t@ype+, bool) =
    Left (a, b, true) of (a)
  | Right (a, b, false) of (b)
stadef either = either_t0ype_bool_type
typedef Either (a:t0p, b:t0p) = [c : bool] either (a, b, c)

fun{a:t0p}{b:t0p} either_left .<>. (a:a):<> either(a, b, true) = Left(a)
fun{a:t0p}{b:t0p} either_right .<>. (b:b):<> either(a, b, false) = Right(b)

When I go to use it

fun do_either(x : int) : [n : nat; m : nat] Either (int n, int m) =
  case+ x of
  | x when x > 0 => either_left(0)
  | x => either_right(1)

implement main0() =
  let
    val _ = do_either(~1)
  in () end

attempts to typecheck this result in

481(line=15, offs=21) -- 511(line=15, offs=51): error(3): unsolved constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(7), S2Eintinf(0)))

I’ve finally understood the reason for this. A call to either_left
will be able to infer the type for the left side (a) as int 0, which
satisfies the n >= 0 constraint that nat has. However, either
still requires a type for the right hand side (b), which has no
constraints put upon it in this case, so the constraint solving fails
showing that we cannot prove that the type for the right side satisfies
that the integer will provably be >= 0.

However, I can’t figure out how to solve this. My feeble attempts to do
either_left<[x:nat] int x>(0) fail, and I feel like there should be a
clear way to solve this?

2

Great, I added clarifications for operators here
https://github.com/githwxi/ATS-Postiats/wiki/Built-in-operators and
linked to both examples on the typechecking errors page (also included some
other recent examples/discussion there).

Brandon Barker
brandon…@gmail.comOn Sun, Aug 17, 2014 at 12:12 AM, Hongwei Xi gmh...@gmail.com wrote:

Thanks for pointing out the bug.

As you can tell, this feature is very rarely used :slight_smile:

On Sun, Aug 17, 2014 at 12:08 AM, gmhwxi gmh...@gmail.com wrote:

Thanks for pointing out the bug.

It worked in ATS1 but not in ATS2. I have just fixed it.

If you use ATS2-github, then please git-pull and recompile.

On Saturday, August 16, 2014 11:26:41 PM UTC-4, Brandon Barker wrote:

I tried this example, but seem to have trouble with the seemingly simple
syntax… it could be a problem with me using the git version of Postiats,
but I tried both a several-day old version and the most recent version.

typedef Int = [x:int] int(x)
typedef IntGT0 = [x:nat] int(x)
typedef DubInt = [x:int] int(2x)
typedef Int2 = [x:int] int(xx)

fun
fun1 (x: Int): void = ()

fun
funGT0 (x: IntGT0): void = ()

fun
dubx(x: DubInt): void = ()

fun
fun2 (x: Int2): void = ()

implement main0 () = {
val x1:int(1) = 1
val x2:int(2) = 2

val () = fun1(x1)
val () = funGT0(x1)

(*
This would produce an unsolved constraint due to
equality constraint:

val () = dubx(x2)

Instead we can do: *)

val () = dubx(#[ 1 | x2])
// ^^^^^^^^^^^^^ This gives the following error
//
// d2exp_trup: loc0 = /home/brandon/witness.dats: 495(line=37, offs=15)
– 505(line=37, offs=25)
// d2exp_trup: d2e0 = D2Eexist(S2EXPARGseq(S2Eintinf(1));
D2Evar(x2$72(-1)))
// /home/brandon/ATS-Postiats/src/pats_trans3_dynexp_up.dats:
12611(line=490, offs=5) – 12621(line=490, offs=15)

}

On Friday, August 15, 2014 11:00:29 PM UTC-4, gmhwxi wrote:

Say you have an expression exp of type int(1).
Say you have a function foo of type Int → void

Note Int = [x:int] int(x).

If you do foo(exp), then the typechecker needs to check
that exp can be given the type Int. In this case, the typechecker
figures out that int(1) can be coerced into Int by setting the witness
x to 1.

Say Int2 = [x:int] int(x*x), and foo2 is of the type Int2 → void.
If you write foo2(exp), the typechecker cannot figure out that int(1)
can
be coerced into Int2. Instead, you need to write foo2(#[1 | exp]) (or
foo2(#[~1 | exp])
to indicate to the typechecker that x needs to be set to 1 (or ~1) for
checking
whether int(1) can be coerced into Int2.

On Friday, August 15, 2014 10:12:29 PM UTC-4, Alex Miller wrote:

The syntax #[… | …] allows you to provide witnesses
explicitly.

IT COMPILES!!!

I don’t quite understand exactly what #[] means though. I’ve found
a
few uses of it throughout doc/, but I can’t seem to find a description
of what the syntax actually means in the ATS book or elsewhere, and
I’m
having trouble reasoning it out. Would you mind explaining a bit?
How
is this different than providing the type via static/template
arguments
(e.g. #[0 | either_left(0)] vs either_left<int 0>(0))?

Dependent types are demanding because handling quantifiers is a lot
harder
than handling propositions (simple types).

I still much prefer writing proofs than tests. I also feel much more
comfortable about my code correctness at the end. :slight_smile:

On Aug 16 2014 at 01:10AM UTC, gmhwxi wrote:

I tidied up the code a bit:

datatype
either_t0ype_bool_type
(
a:t@ype+, b:t@ype+, bool
) =
| Left (a, b, true) of (a)
| Right (a, b, false) of (b)

stadef
either = either_t0ype_bool_type
typedef
either (a:t0p, b:t0p) = [c:bool] either(a, b, c)

fn{
a,b:t0p
} either_left (a:a):<> either(a, b, true) = Left(a)

fn{
a,b:t0p
} either_right (b:b):<> either(a, b, false) = Right(b)

fun do_either(x : int)
: [n:nat; m:nat] either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 |
either_right(1)]

implement main0() = ignoret(do_either(~1))

Even a simple example like this would take a lot of effort :slight_smile:

Dependent types are demanding because handling quantifiers is a lot
harder
than handling
propositions (simple types).

On Friday, August 15, 2014 8:58:02 PM UTC-4, gmhwxi wrote:

This one works:

fun do_either(x : int)
: [n:nat; m:nat] Either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 |
either_right(1)]

The syntax #[… | …] allows you to provide witnesses
explicitly.

On Friday, August 15, 2014 8:48:25 PM UTC-4, Alex Miller wrote:

The following is a minimal example of a typechecking issue I’ve
been
chasing after for a while. I have an either type that I’ve
implemented,
mimicing the standard library’s option type:

datatype either_t0ype_bool_type
  (a : t@ype+, b : t@ype+, bool) =
    Left (a, b, true) of (a)
  | Right (a, b, false) of (b)
stadef either = either_t0ype_bool_type
typedef Either (a:t0p, b:t0p) = [c : bool] either (a, b, c)

fun{a:t0p}{b:t0p} either_left .<>. (a:a):<> either(a, b,

true) =

Left(a)
fun{a:t0p}{b:t0p} either_right .<>. (b:b):<> either(a, b,
false) =
Right(b)

When I go to use it

fun do_either(x : int) : [n : nat; m : nat] Either (int n,

int m) =

  case+ x of
  | x when x > 0 => either_left(0)
  | x => either_right(1)

implement main0() =
  let
    val _ = do_either(~1)
  in () end

attempts to typecheck this result in

481(line=15, offs=21) -- 511(line=15, offs=51): error(3):

unsolved

constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(7),
S2Eintinf(0)))

I’ve finally understood the reason for this. A call to
either_left
will be able to infer the type for the left side (a) as int 0, which
satisfies the n >= 0 constraint that nat has. However,
either
still requires a type for the right hand side (b), which has no
constraints put upon it in this case, so the constraint solving
fails
showing that we cannot prove that the type for the right side
satisfies
that the integer will provably be >= 0.

However, I can’t figure out how to solve this. My feeble
attempts to do
either_left<[x:nat] int x>(0) fail, and I feel like there
should be a
clear way to solve this?

–
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/CAPPSPLqtf%2BUvge-L_-edvXQskWwrV651HB_H2Jh3HEjiOkxJng%40mail.gmail.com
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLqtf%2BUvge-L_-edvXQskWwrV651HB_H2Jh3HEjiOkxJng%40mail.gmail.com?utm_medium=email&utm_source=footer
.

3

Hm, the code that’s being pointed at in the compiler here looks like:

implement
d2exp_trup
  (d2e0) = let
//
val loc0 = d2e0.d2exp_loc
//
val d3e0 = (
case+ d2e0.d2exp_node of

(*** Lots of cases snipped *)

//
| _ => let 
    val () = println! ("d2exp_trup: loc0 = ", loc0)
    val () = println! ("d2exp_trup: d2e0 = ", d2e0)
  in
    exitloc (1)
  end // end of [_]
//
) : d3exp

which very much seems like this falls into the category of “things that
should work, but aren’t actually implemented in the compiler yet” ?On Aug 17 2014 at 03:26AM UTC, Brandon Barker wrote:

I tried this example, but seem to have trouble with the seemingly simple
syntax… it could be a problem with me using the git version of Postiats,
but I tried both a several-day old version and the most recent version.

typedef Int = [x:int] int(x)
typedef IntGT0 = [x:nat] int(x)
typedef DubInt = [x:int] int(2x)
typedef Int2 = [x:int] int(xx)

fun
fun1 (x: Int): void = ()

fun
funGT0 (x: IntGT0): void = ()

fun
dubx(x: DubInt): void = ()

fun
fun2 (x: Int2): void = ()

implement main0 () = {
val x1:int(1) = 1
val x2:int(2) = 2

val () = fun1(x1)
val () = funGT0(x1)

(*
This would produce an unsolved constraint due to
equality constraint:

val () = dubx(x2)

Instead we can do: *)

val () = dubx(#[ 1 | x2])
// ^^^^^^^^^^^^^ This gives the following error
//
// d2exp_trup: loc0 = /home/brandon/witness.dats: 495(line=37, offs=15) –
505(line=37, offs=25)
// d2exp_trup: d2e0 = D2Eexist(S2EXPARGseq(S2Eintinf(1)); D2Evar(x2$72(-1)))
// /home/brandon/ATS-Postiats/src/pats_trans3_dynexp_up.dats:
12611(line=490, offs=5) – 12621(line=490, offs=15)

}

On Friday, August 15, 2014 11:00:29 PM UTC-4, gmhwxi wrote:

Say you have an expression exp of type int(1).
Say you have a function foo of type Int → void

Note Int = [x:int] int(x).

If you do foo(exp), then the typechecker needs to check
that exp can be given the type Int. In this case, the typechecker
figures out that int(1) can be coerced into Int by setting the witness x
to 1.

Say Int2 = [x:int] int(x*x), and foo2 is of the type Int2 → void.
If you write foo2(exp), the typechecker cannot figure out that int(1) can
be coerced into Int2. Instead, you need to write foo2(#[1 | exp]) (or
foo2(#[~1 | exp])
to indicate to the typechecker that x needs to be set to 1 (or ~1) for
checking
whether int(1) can be coerced into Int2.

On Friday, August 15, 2014 10:12:29 PM UTC-4, Alex Miller wrote:

The syntax #[… | …] allows you to provide witnesses explicitly.

IT COMPILES!!!

I don’t quite understand exactly what #[] means though. I’ve found a
few uses of it throughout doc/, but I can’t seem to find a description
of what the syntax actually means in the ATS book or elsewhere, and I’m
having trouble reasoning it out. Would you mind explaining a bit? How
is this different than providing the type via static/template arguments
(e.g. #[0 | either_left(0)] vs either_left<int 0>(0))?

Dependent types are demanding because handling quantifiers is a lot
harder
than handling propositions (simple types).

I still much prefer writing proofs than tests. I also feel much more
comfortable about my code correctness at the end. :slight_smile:

On Aug 16 2014 at 01:10AM UTC, gmhwxi wrote:

I tidied up the code a bit:

datatype
either_t0ype_bool_type
(
a:t@ype+, b:t@ype+, bool
) =
| Left (a, b, true) of (a)
| Right (a, b, false) of (b)

stadef
either = either_t0ype_bool_type
typedef
either (a:t0p, b:t0p) = [c:bool] either(a, b, c)

fn{
a,b:t0p
} either_left (a:a):<> either(a, b, true) = Left(a)

fn{
a,b:t0p
} either_right (b:b):<> either(a, b, false) = Right(b)

fun do_either(x : int)
: [n:nat; m:nat] either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

implement main0() = ignoret(do_either(~1))

Even a simple example like this would take a lot of effort :slight_smile:

Dependent types are demanding because handling quantifiers is a lot
harder
than handling
propositions (simple types).

On Friday, August 15, 2014 8:58:02 PM UTC-4, gmhwxi wrote:

This one works:

fun do_either(x : int)
: [n:nat; m:nat] Either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 |
either_right(1)]

The syntax #[… | …] allows you to provide witnesses explicitly.

On Friday, August 15, 2014 8:48:25 PM UTC-4, Alex Miller wrote:

The following is a minimal example of a typechecking issue I’ve been
chasing after for a while. I have an either type that I’ve
implemented,
mimicing the standard library’s option type:

datatype either_t0ype_bool_type 
  (a : t@ype+, b : t@ype+, bool) = 
    Left (a, b, true) of (a) 
  | Right (a, b, false) of (b) 
stadef either = either_t0ype_bool_type 
typedef Either (a:t0p, b:t0p) = [c : bool] either (a, b, c) 

fun{a:t0p}{b:t0p} either_left .<>. (a:a):<> either(a, b, true) =

Left(a)
fun{a:t0p}{b:t0p} either_right .<>. (b:b):<> either(a, b, false)
=
Right(b)

When I go to use it

fun do_either(x : int) : [n : nat; m : nat] Either (int n, int

m) =

  case+ x of 
  | x when x > 0 => either_left(0) 
  | x => either_right(1) 

implement main0() = 
  let 
    val _ = do_either(~1) 
  in () end

attempts to typecheck this result in

481(line=15, offs=21) -- 511(line=15, offs=51): error(3):

unsolved

constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(7),
S2Eintinf(0)))

I’ve finally understood the reason for this. A call to
either_left
will be able to infer the type for the left side (a) as int 0,
which
satisfies the n >= 0 constraint that nat has. However, either
still requires a type for the right hand side (b), which has no
constraints put upon it in this case, so the constraint solving
fails
showing that we cannot prove that the type for the right side
satisfies
that the integer will provably be >= 0.

However, I can’t figure out how to solve this. My feeble attempts
to do
either_left<[x:nat] int x>(0) fail, and I feel like there should
be a
clear way to solve this?

4

(But, the working either example posted above does typecheck for me.)On Saturday, August 16, 2014 11:26:41 PM UTC-4, Brandon Barker wrote:

I tried this example, but seem to have trouble with the seemingly simple
syntax… it could be a problem with me using the git version of Postiats,
but I tried both a several-day old version and the most recent version.

typedef Int = [x:int] int(x)
typedef IntGT0 = [x:nat] int(x)
typedef DubInt = [x:int] int(2x)
typedef Int2 = [x:int] int(xx)

fun
fun1 (x: Int): void = ()

fun
funGT0 (x: IntGT0): void = ()

fun
dubx(x: DubInt): void = ()

fun
fun2 (x: Int2): void = ()

implement main0 () = {
val x1:int(1) = 1
val x2:int(2) = 2

val () = fun1(x1)
val () = funGT0(x1)

(*
This would produce an unsolved constraint due to
equality constraint:

val () = dubx(x2)

Instead we can do: *)

val () = dubx(#[ 1 | x2])
// ^^^^^^^^^^^^^ This gives the following error
//
// d2exp_trup: loc0 = /home/brandon/witness.dats: 495(line=37, offs=15)
– 505(line=37, offs=25)
// d2exp_trup: d2e0 = D2Eexist(S2EXPARGseq(S2Eintinf(1));
D2Evar(x2$72(-1)))
// /home/brandon/ATS-Postiats/src/pats_trans3_dynexp_up.dats:
12611(line=490, offs=5) – 12621(line=490, offs=15)

}

On Friday, August 15, 2014 11:00:29 PM UTC-4, gmhwxi wrote:

Say you have an expression exp of type int(1).
Say you have a function foo of type Int → void

Note Int = [x:int] int(x).

If you do foo(exp), then the typechecker needs to check
that exp can be given the type Int. In this case, the typechecker
figures out that int(1) can be coerced into Int by setting the witness x
to 1.

Say Int2 = [x:int] int(x*x), and foo2 is of the type Int2 → void.
If you write foo2(exp), the typechecker cannot figure out that int(1) can
be coerced into Int2. Instead, you need to write foo2(#[1 | exp]) (or
foo2(#[~1 | exp])
to indicate to the typechecker that x needs to be set to 1 (or ~1) for
checking
whether int(1) can be coerced into Int2.

On Friday, August 15, 2014 10:12:29 PM UTC-4, Alex Miller wrote:

The syntax #[… | …] allows you to provide witnesses explicitly.

IT COMPILES!!!

I don’t quite understand exactly what #[] means though. I’ve found a
few uses of it throughout doc/, but I can’t seem to find a description
of what the syntax actually means in the ATS book or elsewhere, and I’m
having trouble reasoning it out. Would you mind explaining a bit? How
is this different than providing the type via static/template arguments
(e.g. #[0 | either_left(0)] vs either_left<int 0>(0))?

Dependent types are demanding because handling quantifiers is a lot
harder
than handling propositions (simple types).

I still much prefer writing proofs than tests. I also feel much more
comfortable about my code correctness at the end. :slight_smile:

On Aug 16 2014 at 01:10AM UTC, gmhwxi wrote:

I tidied up the code a bit:

datatype
either_t0ype_bool_type
(
a:t@ype+, b:t@ype+, bool
) =
| Left (a, b, true) of (a)
| Right (a, b, false) of (b)

stadef
either = either_t0ype_bool_type
typedef
either (a:t0p, b:t0p) = [c:bool] either(a, b, c)

fn{
a,b:t0p
} either_left (a:a):<> either(a, b, true) = Left(a)

fn{
a,b:t0p
} either_right (b:b):<> either(a, b, false) = Right(b)

fun do_either(x : int)
: [n:nat; m:nat] either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

implement main0() = ignoret(do_either(~1))

Even a simple example like this would take a lot of effort :slight_smile:

Dependent types are demanding because handling quantifiers is a lot
harder
than handling
propositions (simple types).

On Friday, August 15, 2014 8:58:02 PM UTC-4, gmhwxi wrote:

This one works:

fun do_either(x : int)
: [n:nat; m:nat] Either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 |
either_right(1)]

The syntax #[… | …] allows you to provide witnesses explicitly.

On Friday, August 15, 2014 8:48:25 PM UTC-4, Alex Miller wrote:

The following is a minimal example of a typechecking issue I’ve
been
chasing after for a while. I have an either type that I’ve
implemented,
mimicing the standard library’s option type:

datatype either_t0ype_bool_type 
  (a : t@ype+, b : t@ype+, bool) = 
    Left (a, b, true) of (a) 
  | Right (a, b, false) of (b) 
stadef either = either_t0ype_bool_type 
typedef Either (a:t0p, b:t0p) = [c : bool] either (a, b, c) 

fun{a:t0p}{b:t0p} either_left .<>. (a:a):<> either(a, b, true)

=

Left(a)
fun{a:t0p}{b:t0p} either_right .<>. (b:b):<> either(a, b,
false) =
Right(b)

When I go to use it

fun do_either(x : int) : [n : nat; m : nat] Either (int n, int

m) =

  case+ x of 
  | x when x > 0 => either_left(0) 
  | x => either_right(1) 

implement main0() = 
  let 
    val _ = do_either(~1) 
  in () end

attempts to typecheck this result in

481(line=15, offs=21) -- 511(line=15, offs=51): error(3):

unsolved

constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(7),
S2Eintinf(0)))

I’ve finally understood the reason for this. A call to
either_left
will be able to infer the type for the left side (a) as int 0,
which
satisfies the n >= 0 constraint that nat has. However,
either
still requires a type for the right hand side (b), which has no
constraints put upon it in this case, so the constraint solving
fails
showing that we cannot prove that the type for the right side
satisfies
that the integer will provably be >= 0.

However, I can’t figure out how to solve this. My feeble attempts
to do
either_left<[x:nat] int x>(0) fail, and I feel like there should
be a
clear way to solve this?

5

Ah, that would probably do it … there was even a comment, if only i’d
looked.

Brandon Barker
brandon…@gmail.comOn Sat, Aug 16, 2014 at 5:03 PM, Alex Miller mille...@gmail.com wrote:

Hm, the code that’s being pointed at in the compiler here looks like:

implement
d2exp_trup
  (d2e0) = let
//
val loc0 = d2e0.d2exp_loc
//
val d3e0 = (
case+ d2e0.d2exp_node of

(*** Lots of cases snipped *)

//
| _ => let
    val () = println! ("d2exp_trup: loc0 = ", loc0)
    val () = println! ("d2exp_trup: d2e0 = ", d2e0)
  in
    exitloc (1)
  end // end of [_]
//
) : d3exp

which very much seems like this falls into the category of “things that
should work, but aren’t actually implemented in the compiler yet” ?

On Aug 17 2014 at 03:26AM UTC, Brandon Barker wrote:

I tried this example, but seem to have trouble with the seemingly simple
syntax… it could be a problem with me using the git version of
Postiats,
but I tried both a several-day old version and the most recent version.

typedef Int = [x:int] int(x)
typedef IntGT0 = [x:nat] int(x)
typedef DubInt = [x:int] int(2x)
typedef Int2 = [x:int] int(xx)

fun
fun1 (x: Int): void = ()

fun
funGT0 (x: IntGT0): void = ()

fun
dubx(x: DubInt): void = ()

fun
fun2 (x: Int2): void = ()

implement main0 () = {
val x1:int(1) = 1
val x2:int(2) = 2

val () = fun1(x1)
val () = funGT0(x1)

(*
This would produce an unsolved constraint due to
equality constraint:

val () = dubx(x2)

Instead we can do: *)

val () = dubx(#[ 1 | x2])
// ^^^^^^^^^^^^^ This gives the following error
//
// d2exp_trup: loc0 = /home/brandon/witness.dats: 495(line=37, offs=15)
–
505(line=37, offs=25)
// d2exp_trup: d2e0 = D2Eexist(S2EXPARGseq(S2Eintinf(1));
D2Evar(x2$72(-1)))
// /home/brandon/ATS-Postiats/src/pats_trans3_dynexp_up.dats:
12611(line=490, offs=5) – 12621(line=490, offs=15)

}

On Friday, August 15, 2014 11:00:29 PM UTC-4, gmhwxi wrote:

Say you have an expression exp of type int(1).
Say you have a function foo of type Int → void

Note Int = [x:int] int(x).

If you do foo(exp), then the typechecker needs to check
that exp can be given the type Int. In this case, the typechecker
figures out that int(1) can be coerced into Int by setting the witness
x
to 1.

Say Int2 = [x:int] int(x*x), and foo2 is of the type Int2 → void.
If you write foo2(exp), the typechecker cannot figure out that int(1)
can
be coerced into Int2. Instead, you need to write foo2(#[1 | exp]) (or
foo2(#[~1 | exp])
to indicate to the typechecker that x needs to be set to 1 (or ~1) for
checking
whether int(1) can be coerced into Int2.

On Friday, August 15, 2014 10:12:29 PM UTC-4, Alex Miller wrote:

The syntax #[… | …] allows you to provide witnesses
explicitly.

IT COMPILES!!!

I don’t quite understand exactly what #[] means though. I’ve found
a
few uses of it throughout doc/, but I can’t seem to find a description
of what the syntax actually means in the ATS book or elsewhere, and
I’m
having trouble reasoning it out. Would you mind explaining a bit?
How
is this different than providing the type via static/template
arguments
(e.g. #[0 | either_left(0)] vs either_left<int 0>(0))?

Dependent types are demanding because handling quantifiers is a lot
harder
than handling propositions (simple types).

I still much prefer writing proofs than tests. I also feel much more
comfortable about my code correctness at the end. :slight_smile:

On Aug 16 2014 at 01:10AM UTC, gmhwxi wrote:

I tidied up the code a bit:

datatype
either_t0ype_bool_type
(
a:t@ype+, b:t@ype+, bool
) =
| Left (a, b, true) of (a)
| Right (a, b, false) of (b)

stadef
either = either_t0ype_bool_type
typedef
either (a:t0p, b:t0p) = [c:bool] either(a, b, c)

fn{
a,b:t0p
} either_left (a:a):<> either(a, b, true) = Left(a)

fn{
a,b:t0p
} either_right (b:b):<> either(a, b, false) = Right(b)

fun do_either(x : int)
: [n:nat; m:nat] either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 |
either_right(1)]

implement main0() = ignoret(do_either(~1))

Even a simple example like this would take a lot of effort :slight_smile:

Dependent types are demanding because handling quantifiers is a lot
harder
than handling
propositions (simple types).

On Friday, August 15, 2014 8:58:02 PM UTC-4, gmhwxi wrote:

This one works:

fun do_either(x : int)
: [n:nat; m:nat] Either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 |
either_right(1)]

The syntax #[… | …] allows you to provide witnesses
explicitly.

On Friday, August 15, 2014 8:48:25 PM UTC-4, Alex Miller wrote:

The following is a minimal example of a typechecking issue I’ve
been
chasing after for a while. I have an either type that I’ve
implemented,
mimicing the standard library’s option type:

datatype either_t0ype_bool_type
  (a : t@ype+, b : t@ype+, bool) =
    Left (a, b, true) of (a)
  | Right (a, b, false) of (b)
stadef either = either_t0ype_bool_type
typedef Either (a:t0p, b:t0p) = [c : bool] either (a, b, c)

fun{a:t0p}{b:t0p} either_left .<>. (a:a):<> either(a, b,

true) =

Left(a)
fun{a:t0p}{b:t0p} either_right .<>. (b:b):<> either(a, b,
false)
=
Right(b)

When I go to use it

fun do_either(x : int) : [n : nat; m : nat] Either (int n,

int

m) =

  case+ x of
  | x when x > 0 => either_left(0)
  | x => either_right(1)

implement main0() =
  let
    val _ = do_either(~1)
  in () end

attempts to typecheck this result in

481(line=15, offs=21) -- 511(line=15, offs=51): error(3):

unsolved

constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(7),
S2Eintinf(0)))

I’ve finally understood the reason for this. A call to
either_left
will be able to infer the type for the left side (a) as int 0,
which
satisfies the n >= 0 constraint that nat has. However,
either
still requires a type for the right hand side (b), which has no
constraints put upon it in this case, so the constraint solving
fails
showing that we cannot prove that the type for the right side
satisfies
that the integer will provably be >= 0.

However, I can’t figure out how to solve this. My feeble
attempts
to do
either_left<[x:nat] int x>(0) fail, and I feel like there
should
be a
clear way to solve this?

–
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/1408222345-sup-8542%40IAmLaptop
.

6

I tried this example, but seem to have trouble with the seemingly simple
syntax… it could be a problem with me using the git version of Postiats,
but I tried both a several-day old version and the most recent version.

typedef Int = [x:int] int(x)
typedef IntGT0 = [x:nat] int(x)
typedef DubInt = [x:int] int(2x)
typedef Int2 = [x:int] int(xx)

fun
fun1 (x: Int): void = ()

fun
funGT0 (x: IntGT0): void = ()

fun
dubx(x: DubInt): void = ()

fun
fun2 (x: Int2): void = ()

implement main0 () = {
val x1:int(1) = 1
val x2:int(2) = 2

val () = fun1(x1)
val () = funGT0(x1)

(*
This would produce an unsolved constraint due to
equality constraint:

val () = dubx(x2)

Instead we can do: *)

val () = dubx(#[ 1 | x2])
// ^^^^^^^^^^^^^ This gives the following error
//
// d2exp_trup: loc0 = /home/brandon/witness.dats: 495(line=37, offs=15) –
505(line=37, offs=25)
// d2exp_trup: d2e0 = D2Eexist(S2EXPARGseq(S2Eintinf(1)); D2Evar(x2$72(-1)))
// /home/brandon/ATS-Postiats/src/pats_trans3_dynexp_up.dats:
12611(line=490, offs=5) – 12621(line=490, offs=15)

}On Friday, August 15, 2014 11:00:29 PM UTC-4, gmhwxi wrote:

Say you have an expression exp of type int(1).
Say you have a function foo of type Int → void

Note Int = [x:int] int(x).

If you do foo(exp), then the typechecker needs to check
that exp can be given the type Int. In this case, the typechecker
figures out that int(1) can be coerced into Int by setting the witness x
to 1.

Say Int2 = [x:int] int(x*x), and foo2 is of the type Int2 → void.
If you write foo2(exp), the typechecker cannot figure out that int(1) can
be coerced into Int2. Instead, you need to write foo2(#[1 | exp]) (or
foo2(#[~1 | exp])
to indicate to the typechecker that x needs to be set to 1 (or ~1) for
checking
whether int(1) can be coerced into Int2.

On Friday, August 15, 2014 10:12:29 PM UTC-4, Alex Miller wrote:

The syntax #[… | …] allows you to provide witnesses explicitly.

IT COMPILES!!!

I don’t quite understand exactly what #[] means though. I’ve found a
few uses of it throughout doc/, but I can’t seem to find a description
of what the syntax actually means in the ATS book or elsewhere, and I’m
having trouble reasoning it out. Would you mind explaining a bit? How
is this different than providing the type via static/template arguments
(e.g. #[0 | either_left(0)] vs either_left<int 0>(0))?

Dependent types are demanding because handling quantifiers is a lot
harder
than handling propositions (simple types).

I still much prefer writing proofs than tests. I also feel much more
comfortable about my code correctness at the end. :slight_smile:

On Aug 16 2014 at 01:10AM UTC, gmhwxi wrote:

I tidied up the code a bit:

datatype
either_t0ype_bool_type
(
a:t@ype+, b:t@ype+, bool
) =
| Left (a, b, true) of (a)
| Right (a, b, false) of (b)

stadef
either = either_t0ype_bool_type
typedef
either (a:t0p, b:t0p) = [c:bool] either(a, b, c)

fn{
a,b:t0p
} either_left (a:a):<> either(a, b, true) = Left(a)

fn{
a,b:t0p
} either_right (b:b):<> either(a, b, false) = Right(b)

fun do_either(x : int)
: [n:nat; m:nat] either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

implement main0() = ignoret(do_either(~1))

Even a simple example like this would take a lot of effort :slight_smile:

Dependent types are demanding because handling quantifiers is a lot
harder
than handling
propositions (simple types).

On Friday, August 15, 2014 8:58:02 PM UTC-4, gmhwxi wrote:

This one works:

fun do_either(x : int)
: [n:nat; m:nat] Either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 |
either_right(1)]

The syntax #[… | …] allows you to provide witnesses explicitly.

On Friday, August 15, 2014 8:48:25 PM UTC-4, Alex Miller wrote:

The following is a minimal example of a typechecking issue I’ve been
chasing after for a while. I have an either type that I’ve
implemented,
mimicing the standard library’s option type:

datatype either_t0ype_bool_type 
  (a : t@ype+, b : t@ype+, bool) = 
    Left (a, b, true) of (a) 
  | Right (a, b, false) of (b) 
stadef either = either_t0ype_bool_type 
typedef Either (a:t0p, b:t0p) = [c : bool] either (a, b, c) 

fun{a:t0p}{b:t0p} either_left .<>. (a:a):<> either(a, b, true) =

Left(a)
fun{a:t0p}{b:t0p} either_right .<>. (b:b):<> either(a, b, false)
=
Right(b)

When I go to use it

fun do_either(x : int) : [n : nat; m : nat] Either (int n, int

m) =

  case+ x of 
  | x when x > 0 => either_left(0) 
  | x => either_right(1) 

implement main0() = 
  let 
    val _ = do_either(~1) 
  in () end

attempts to typecheck this result in

481(line=15, offs=21) -- 511(line=15, offs=51): error(3):

unsolved

constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(7),
S2Eintinf(0)))

I’ve finally understood the reason for this. A call to
either_left
will be able to infer the type for the left side (a) as int 0,
which
satisfies the n >= 0 constraint that nat has. However, either
still requires a type for the right hand side (b), which has no
constraints put upon it in this case, so the constraint solving
fails
showing that we cannot prove that the type for the right side
satisfies
that the integer will provably be >= 0.

However, I can’t figure out how to solve this. My feeble attempts
to do
either_left<[x:nat] int x>(0) fail, and I feel like there should
be a
clear way to solve this?

7

#[…] and #[… | …] are unrelated syntax.On Friday, August 15, 2014 10:32:46 PM UTC-4, Brandon Barker wrote:

The syntax seems to be slightly different here.

Brandon Barker
brand...@gmail.com <javascript:>

On Fri, Aug 15, 2014 at 10:27 PM, Brandon Barker <brand...@gmail.com <javascript:>> wrote:

I had this same trouble before … more than once. Both instances are
buried deep in this mailing list I think.

I wish you luck in finding them, but perhaps the ATS wiki’s explanation
is good enough (it could probably be improved actually):

Built in operators · githwxi/ATS-Postiats Wiki · GitHub

Brandon Barker
brand...@gmail.com <javascript:>

On Fri, Aug 15, 2014 at 3:12 PM, Alex Miller <mill...@gmail.com <javascript:>> wrote:

The syntax #[… | …] allows you to provide witnesses explicitly.

IT COMPILES!!!

I don’t quite understand exactly what #[] means though. I’ve found a
few uses of it throughout doc/, but I can’t seem to find a description
of what the syntax actually means in the ATS book or elsewhere, and I’m
having trouble reasoning it out. Would you mind explaining a bit? How
is this different than providing the type via static/template arguments
(e.g. #[0 | either_left(0)] vs either_left<int 0>(0))?

Dependent types are demanding because handling quantifiers is a lot
harder
than handling propositions (simple types).

I still much prefer writing proofs than tests. I also feel much more
comfortable about my code correctness at the end. :slight_smile:

On Aug 16 2014 at 01:10AM UTC, gmhwxi wrote:

I tidied up the code a bit:

datatype
either_t0ype_bool_type
(
a:t@ype+, b:t@ype+, bool
) =
| Left (a, b, true) of (a)
| Right (a, b, false) of (b)

stadef
either = either_t0ype_bool_type
typedef
either (a:t0p, b:t0p) = [c:bool] either(a, b, c)

fn{
a,b:t0p
} either_left (a:a):<> either(a, b, true) = Left(a)

fn{
a,b:t0p
} either_right (b:b):<> either(a, b, false) = Right(b)

fun do_either(x : int)
: [n:nat; m:nat] either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

implement main0() = ignoret(do_either(~1))

Even a simple example like this would take a lot of effort :slight_smile:

Dependent types are demanding because handling quantifiers is a lot
harder
than handling
propositions (simple types).

On Friday, August 15, 2014 8:58:02 PM UTC-4, gmhwxi wrote:

This one works:

fun do_either(x : int)
: [n:nat; m:nat] Either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 |
either_right(1)]

The syntax #[… | …] allows you to provide witnesses explicitly.

On Friday, August 15, 2014 8:48:25 PM UTC-4, Alex Miller wrote:

The following is a minimal example of a typechecking issue I’ve been
chasing after for a while. I have an either type that I’ve
implemented,
mimicing the standard library’s option type:

datatype either_t0ype_bool_type
  (a : t@ype+, b : t@ype+, bool) =
    Left (a, b, true) of (a)
  | Right (a, b, false) of (b)
stadef either = either_t0ype_bool_type
typedef Either (a:t0p, b:t0p) = [c : bool] either (a, b, c)

fun{a:t0p}{b:t0p} either_left .<>. (a:a):<> either(a, b, true) =

Left(a)
fun{a:t0p}{b:t0p} either_right .<>. (b:b):<> either(a, b,
false) =
Right(b)

When I go to use it

fun do_either(x : int) : [n : nat; m : nat] Either (int n, int

m) =

  case+ x of
  | x when x > 0 => either_left(0)
  | x => either_right(1)

implement main0() =
  let
    val _ = do_either(~1)
  in () end

attempts to typecheck this result in

481(line=15, offs=21) -- 511(line=15, offs=51): error(3):

unsolved

constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(7),
S2Eintinf(0)))

I’ve finally understood the reason for this. A call to
either_left
will be able to infer the type for the left side (a) as int 0,
which
satisfies the n >= 0 constraint that nat has. However, either
still requires a type for the right hand side (b), which has no
constraints put upon it in this case, so the constraint solving
fails
showing that we cannot prove that the type for the right side
satisfies
that the integer will provably be >= 0.

However, I can’t figure out how to solve this. My feeble attempts
to do
either_left<[x:nat] int x>(0) fail, and I feel like there should
be a
clear way to solve this?

–
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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
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/1408128934-sup-4407%40IAmLaptop
.

8

This one works:

fun do_either(x : int)
: [n:nat; m:nat] Either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

The syntax #[… | …] allows you to provide witnesses explicitly.On Friday, August 15, 2014 8:48:25 PM UTC-4, Alex Miller wrote:

The following is a minimal example of a typechecking issue I’ve been
chasing after for a while. I have an either type that I’ve implemented,
mimicing the standard library’s option type:

datatype either_t0ype_bool_type 
  (a : t@ype+, b : t@ype+, bool) = 
    Left (a, b, true) of (a) 
  | Right (a, b, false) of (b) 
stadef either = either_t0ype_bool_type 
typedef Either (a:t0p, b:t0p) = [c : bool] either (a, b, c) 

fun{a:t0p}{b:t0p} either_left .<>. (a:a):<> either(a, b, true) =

Left(a)
fun{a:t0p}{b:t0p} either_right .<>. (b:b):<> either(a, b, false) =
Right(b)

When I go to use it

fun do_either(x : int) : [n : nat; m : nat] Either (int n, int m) = 
  case+ x of 
  | x when x > 0 => either_left(0) 
  | x => either_right(1) 

implement main0() = 
  let 
    val _ = do_either(~1) 
  in () end

attempts to typecheck this result in

481(line=15, offs=21) -- 511(line=15, offs=51): error(3): unsolved

constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(7), S2Eintinf(0)))

I’ve finally understood the reason for this. A call to either_left
will be able to infer the type for the left side (a) as int 0, which
satisfies the n >= 0 constraint that nat has. However, either
still requires a type for the right hand side (b), which has no
constraints put upon it in this case, so the constraint solving fails
showing that we cannot prove that the type for the right side satisfies
that the integer will provably be >= 0.

However, I can’t figure out how to solve this. My feeble attempts to do
either_left<[x:nat] int x>(0) fail, and I feel like there should be a
clear way to solve this?

9

I had this same trouble before … more than once. Both instances are
buried deep in this mailing list I think.

I wish you luck in finding them, but perhaps the ATS wiki’s explanation is
good enough (it could probably be improved actually):

Brandon Barker
brandon…@gmail.comOn Fri, Aug 15, 2014 at 3:12 PM, Alex Miller mille...@gmail.com wrote:

The syntax #[… | …] allows you to provide witnesses explicitly.

IT COMPILES!!!

I don’t quite understand exactly what #[] means though. I’ve found a
few uses of it throughout doc/, but I can’t seem to find a description
of what the syntax actually means in the ATS book or elsewhere, and I’m
having trouble reasoning it out. Would you mind explaining a bit? How
is this different than providing the type via static/template arguments
(e.g. #[0 | either_left(0)] vs either_left<int 0>(0))?

Dependent types are demanding because handling quantifiers is a lot
harder
than handling propositions (simple types).

I still much prefer writing proofs than tests. I also feel much more
comfortable about my code correctness at the end. :slight_smile:

On Aug 16 2014 at 01:10AM UTC, gmhwxi wrote:

I tidied up the code a bit:

datatype
either_t0ype_bool_type
(
a:t@ype+, b:t@ype+, bool
) =
| Left (a, b, true) of (a)
| Right (a, b, false) of (b)

stadef
either = either_t0ype_bool_type
typedef
either (a:t0p, b:t0p) = [c:bool] either(a, b, c)

fn{
a,b:t0p
} either_left (a:a):<> either(a, b, true) = Left(a)

fn{
a,b:t0p
} either_right (b:b):<> either(a, b, false) = Right(b)

fun do_either(x : int)
: [n:nat; m:nat] either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

implement main0() = ignoret(do_either(~1))

Even a simple example like this would take a lot of effort :slight_smile:

Dependent types are demanding because handling quantifiers is a lot
harder
than handling
propositions (simple types).

On Friday, August 15, 2014 8:58:02 PM UTC-4, gmhwxi wrote:

This one works:

fun do_either(x : int)
: [n:nat; m:nat] Either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

The syntax #[… | …] allows you to provide witnesses explicitly.

On Friday, August 15, 2014 8:48:25 PM UTC-4, Alex Miller wrote:

The following is a minimal example of a typechecking issue I’ve been
chasing after for a while. I have an either type that I’ve
implemented,
mimicing the standard library’s option type:

datatype either_t0ype_bool_type
  (a : t@ype+, b : t@ype+, bool) =
    Left (a, b, true) of (a)
  | Right (a, b, false) of (b)
stadef either = either_t0ype_bool_type
typedef Either (a:t0p, b:t0p) = [c : bool] either (a, b, c)

fun{a:t0p}{b:t0p} either_left .<>. (a:a):<> either(a, b, true) =

Left(a)
fun{a:t0p}{b:t0p} either_right .<>. (b:b):<> either(a, b, false) =
Right(b)

When I go to use it

fun do_either(x : int) : [n : nat; m : nat] Either (int n, int m)

=

  case+ x of
  | x when x > 0 => either_left(0)
  | x => either_right(1)

implement main0() =
  let
    val _ = do_either(~1)
  in () end

attempts to typecheck this result in

481(line=15, offs=21) -- 511(line=15, offs=51): error(3): unsolved

constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(7),
S2Eintinf(0)))

I’ve finally understood the reason for this. A call to either_left
will be able to infer the type for the left side (a) as int 0,
which
satisfies the n >= 0 constraint that nat has. However, either
still requires a type for the right hand side (b), which has no
constraints put upon it in this case, so the constraint solving fails
showing that we cannot prove that the type for the right side
satisfies
that the integer will provably be >= 0.

However, I can’t figure out how to solve this. My feeble attempts to
do
either_left<[x:nat] int x>(0) fail, and I feel like there should be
a
clear way to solve this?

–
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/1408128934-sup-4407%40IAmLaptop
.

10

This version works, too:

fun do2_either(x : int)
: [n:nat; m:nat] either (int n, int m) =
if x > 0 then either_left<int(0),int(1)> (0) else either_right<int(0),int(
1)> (1)

either_left<int 0>(0)

You need: either_left<int(0)><int(1)>(0)On Friday, August 15, 2014 10:12:29 PM UTC-4, Alex Miller wrote:

The syntax #[… | …] allows you to provide witnesses explicitly.

IT COMPILES!!!

I don’t quite understand exactly what #[] means though. I’ve found a
few uses of it throughout doc/, but I can’t seem to find a description
of what the syntax actually means in the ATS book or elsewhere, and I’m
having trouble reasoning it out. Would you mind explaining a bit? How
is this different than providing the type via static/template arguments
(e.g. #[0 | either_left(0)] vs either_left<int 0>(0))?

Dependent types are demanding because handling quantifiers is a lot
harder
than handling propositions (simple types).

I still much prefer writing proofs than tests. I also feel much more
comfortable about my code correctness at the end. :slight_smile:

On Aug 16 2014 at 01:10AM UTC, gmhwxi wrote:

I tidied up the code a bit:

datatype
either_t0ype_bool_type
(
a:t@ype+, b:t@ype+, bool
) =
| Left (a, b, true) of (a)
| Right (a, b, false) of (b)

stadef
either = either_t0ype_bool_type
typedef
either (a:t0p, b:t0p) = [c:bool] either(a, b, c)

fn{
a,b:t0p
} either_left (a:a):<> either(a, b, true) = Left(a)

fn{
a,b:t0p
} either_right (b:b):<> either(a, b, false) = Right(b)

fun do_either(x : int)
: [n:nat; m:nat] either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

implement main0() = ignoret(do_either(~1))

Even a simple example like this would take a lot of effort :slight_smile:

Dependent types are demanding because handling quantifiers is a lot
harder
than handling
propositions (simple types).

On Friday, August 15, 2014 8:58:02 PM UTC-4, gmhwxi wrote:

This one works:

fun do_either(x : int)
: [n:nat; m:nat] Either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

The syntax #[… | …] allows you to provide witnesses explicitly.

On Friday, August 15, 2014 8:48:25 PM UTC-4, Alex Miller wrote:

The following is a minimal example of a typechecking issue I’ve been
chasing after for a while. I have an either type that I’ve
implemented,
mimicing the standard library’s option type:

datatype either_t0ype_bool_type 
  (a : t@ype+, b : t@ype+, bool) = 
    Left (a, b, true) of (a) 
  | Right (a, b, false) of (b) 
stadef either = either_t0ype_bool_type 
typedef Either (a:t0p, b:t0p) = [c : bool] either (a, b, c) 

fun{a:t0p}{b:t0p} either_left .<>. (a:a):<> either(a, b, true) =

Left(a)
fun{a:t0p}{b:t0p} either_right .<>. (b:b):<> either(a, b, false)
=
Right(b)

When I go to use it

fun do_either(x : int) : [n : nat; m : nat] Either (int n, int m)

=

  case+ x of 
  | x when x > 0 => either_left(0) 
  | x => either_right(1) 

implement main0() = 
  let 
    val _ = do_either(~1) 
  in () end

attempts to typecheck this result in

481(line=15, offs=21) -- 511(line=15, offs=51): error(3):

unsolved

constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(7),
S2Eintinf(0)))

I’ve finally understood the reason for this. A call to either_left
will be able to infer the type for the left side (a) as int 0,
which
satisfies the n >= 0 constraint that nat has. However, either
still requires a type for the right hand side (b), which has no
constraints put upon it in this case, so the constraint solving fails
showing that we cannot prove that the type for the right side
satisfies
that the integer will provably be >= 0.

However, I can’t figure out how to solve this. My feeble attempts to
do
either_left<[x:nat] int x>(0) fail, and I feel like there should be
a
clear way to solve this?

11

I tidied up the code a bit:

datatype
either_t0ype_bool_type
(
a:t@ype+, b:t@ype+, bool
) =
| Left (a, b, true) of (a)
| Right (a, b, false) of (b)

stadef
either = either_t0ype_bool_type
typedef
either (a:t0p, b:t0p) = [c:bool] either(a, b, c)

fn{
a,b:t0p
} either_left (a:a):<> either(a, b, true) = Left(a)

fn{
a,b:t0p
} either_right (b:b):<> either(a, b, false) = Right(b)

fun do_either(x : int)
: [n:nat; m:nat] either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

implement main0() = ignoret(do_either(~1))

Even a simple example like this would take a lot of effort :slight_smile:

Dependent types are demanding because handling quantifiers is a lot harder
than handling
propositions (simple types).On Friday, August 15, 2014 8:58:02 PM UTC-4, gmhwxi wrote:

This one works:

fun do_either(x : int)
: [n:nat; m:nat] Either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

The syntax #[… | …] allows you to provide witnesses explicitly.

On Friday, August 15, 2014 8:48:25 PM UTC-4, Alex Miller wrote:

The following is a minimal example of a typechecking issue I’ve been
chasing after for a while. I have an either type that I’ve implemented,
mimicing the standard library’s option type:

datatype either_t0ype_bool_type 
  (a : t@ype+, b : t@ype+, bool) = 
    Left (a, b, true) of (a) 
  | Right (a, b, false) of (b) 
stadef either = either_t0ype_bool_type 
typedef Either (a:t0p, b:t0p) = [c : bool] either (a, b, c) 

fun{a:t0p}{b:t0p} either_left .<>. (a:a):<> either(a, b, true) =

Left(a)
fun{a:t0p}{b:t0p} either_right .<>. (b:b):<> either(a, b, false) =
Right(b)

When I go to use it

fun do_either(x : int) : [n : nat; m : nat] Either (int n, int m) = 
  case+ x of 
  | x when x > 0 => either_left(0) 
  | x => either_right(1) 

implement main0() = 
  let 
    val _ = do_either(~1) 
  in () end

attempts to typecheck this result in

481(line=15, offs=21) -- 511(line=15, offs=51): error(3): unsolved

constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(7), S2Eintinf(0)))

I’ve finally understood the reason for this. A call to either_left
will be able to infer the type for the left side (a) as int 0, which
satisfies the n >= 0 constraint that nat has. However, either
still requires a type for the right hand side (b), which has no
constraints put upon it in this case, so the constraint solving fails
showing that we cannot prove that the type for the right side satisfies
that the integer will provably be >= 0.

However, I can’t figure out how to solve this. My feeble attempts to do
either_left<[x:nat] int x>(0) fail, and I feel like there should be a
clear way to solve this?

12

Thanks for pointing out the bug.

It worked in ATS1 but not in ATS2. I have just fixed it.

If you use ATS2-github, then please git-pull and recompile.On Saturday, August 16, 2014 11:26:41 PM UTC-4, Brandon Barker wrote:

I tried this example, but seem to have trouble with the seemingly simple
syntax… it could be a problem with me using the git version of Postiats,
but I tried both a several-day old version and the most recent version.

typedef Int = [x:int] int(x)
typedef IntGT0 = [x:nat] int(x)
typedef DubInt = [x:int] int(2x)
typedef Int2 = [x:int] int(xx)

fun
fun1 (x: Int): void = ()

fun
funGT0 (x: IntGT0): void = ()

fun
dubx(x: DubInt): void = ()

fun
fun2 (x: Int2): void = ()

implement main0 () = {
val x1:int(1) = 1
val x2:int(2) = 2

val () = fun1(x1)
val () = funGT0(x1)

(*
This would produce an unsolved constraint due to
equality constraint:

val () = dubx(x2)

Instead we can do: *)

val () = dubx(#[ 1 | x2])
// ^^^^^^^^^^^^^ This gives the following error
//
// d2exp_trup: loc0 = /home/brandon/witness.dats: 495(line=37, offs=15)
– 505(line=37, offs=25)
// d2exp_trup: d2e0 = D2Eexist(S2EXPARGseq(S2Eintinf(1));
D2Evar(x2$72(-1)))
// /home/brandon/ATS-Postiats/src/pats_trans3_dynexp_up.dats:
12611(line=490, offs=5) – 12621(line=490, offs=15)

}

On Friday, August 15, 2014 11:00:29 PM UTC-4, gmhwxi wrote:

Say you have an expression exp of type int(1).
Say you have a function foo of type Int → void

Note Int = [x:int] int(x).

If you do foo(exp), then the typechecker needs to check
that exp can be given the type Int. In this case, the typechecker
figures out that int(1) can be coerced into Int by setting the witness x
to 1.

Say Int2 = [x:int] int(x*x), and foo2 is of the type Int2 → void.
If you write foo2(exp), the typechecker cannot figure out that int(1) can
be coerced into Int2. Instead, you need to write foo2(#[1 | exp]) (or
foo2(#[~1 | exp])
to indicate to the typechecker that x needs to be set to 1 (or ~1) for
checking
whether int(1) can be coerced into Int2.

On Friday, August 15, 2014 10:12:29 PM UTC-4, Alex Miller wrote:

The syntax #[… | …] allows you to provide witnesses explicitly.

IT COMPILES!!!

I don’t quite understand exactly what #[] means though. I’ve found a
few uses of it throughout doc/, but I can’t seem to find a description
of what the syntax actually means in the ATS book or elsewhere, and I’m
having trouble reasoning it out. Would you mind explaining a bit? How
is this different than providing the type via static/template arguments
(e.g. #[0 | either_left(0)] vs either_left<int 0>(0))?

Dependent types are demanding because handling quantifiers is a lot
harder
than handling propositions (simple types).

I still much prefer writing proofs than tests. I also feel much more
comfortable about my code correctness at the end. :slight_smile:

On Aug 16 2014 at 01:10AM UTC, gmhwxi wrote:

I tidied up the code a bit:

datatype
either_t0ype_bool_type
(
a:t@ype+, b:t@ype+, bool
) =
| Left (a, b, true) of (a)
| Right (a, b, false) of (b)

stadef
either = either_t0ype_bool_type
typedef
either (a:t0p, b:t0p) = [c:bool] either(a, b, c)

fn{
a,b:t0p
} either_left (a:a):<> either(a, b, true) = Left(a)

fn{
a,b:t0p
} either_right (b:b):<> either(a, b, false) = Right(b)

fun do_either(x : int)
: [n:nat; m:nat] either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

implement main0() = ignoret(do_either(~1))

Even a simple example like this would take a lot of effort :slight_smile:

Dependent types are demanding because handling quantifiers is a lot
harder
than handling
propositions (simple types).

On Friday, August 15, 2014 8:58:02 PM UTC-4, gmhwxi wrote:

This one works:

fun do_either(x : int)
: [n:nat; m:nat] Either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 |
either_right(1)]

The syntax #[… | …] allows you to provide witnesses explicitly.

On Friday, August 15, 2014 8:48:25 PM UTC-4, Alex Miller wrote:

The following is a minimal example of a typechecking issue I’ve
been
chasing after for a while. I have an either type that I’ve
implemented,
mimicing the standard library’s option type:

datatype either_t0ype_bool_type 
  (a : t@ype+, b : t@ype+, bool) = 
    Left (a, b, true) of (a) 
  | Right (a, b, false) of (b) 
stadef either = either_t0ype_bool_type 
typedef Either (a:t0p, b:t0p) = [c : bool] either (a, b, c) 

fun{a:t0p}{b:t0p} either_left .<>. (a:a):<> either(a, b, true)

=

Left(a)
fun{a:t0p}{b:t0p} either_right .<>. (b:b):<> either(a, b,
false) =
Right(b)

When I go to use it

fun do_either(x : int) : [n : nat; m : nat] Either (int n, int

m) =

  case+ x of 
  | x when x > 0 => either_left(0) 
  | x => either_right(1) 

implement main0() = 
  let 
    val _ = do_either(~1) 
  in () end

attempts to typecheck this result in

481(line=15, offs=21) -- 511(line=15, offs=51): error(3):

unsolved

constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(7),
S2Eintinf(0)))

I’ve finally understood the reason for this. A call to
either_left
will be able to infer the type for the left side (a) as int 0,
which
satisfies the n >= 0 constraint that nat has. However,
either
still requires a type for the right hand side (b), which has no
constraints put upon it in this case, so the constraint solving
fails
showing that we cannot prove that the type for the right side
satisfies
that the integer will provably be >= 0.

However, I can’t figure out how to solve this. My feeble attempts
to do
either_left<[x:nat] int x>(0) fail, and I feel like there should
be a
clear way to solve this?

13

Thanks for pointing out the bug.

As you can tell, this feature is very rarely used :)On Sun, Aug 17, 2014 at 12:08 AM, gmhwxi gmh...@gmail.com wrote:

Thanks for pointing out the bug.

It worked in ATS1 but not in ATS2. I have just fixed it.

If you use ATS2-github, then please git-pull and recompile.

On Saturday, August 16, 2014 11:26:41 PM UTC-4, Brandon Barker wrote:

I tried this example, but seem to have trouble with the seemingly simple
syntax… it could be a problem with me using the git version of Postiats,
but I tried both a several-day old version and the most recent version.

typedef Int = [x:int] int(x)
typedef IntGT0 = [x:nat] int(x)
typedef DubInt = [x:int] int(2x)
typedef Int2 = [x:int] int(xx)

fun
fun1 (x: Int): void = ()

fun
funGT0 (x: IntGT0): void = ()

fun
dubx(x: DubInt): void = ()

fun
fun2 (x: Int2): void = ()

implement main0 () = {
val x1:int(1) = 1
val x2:int(2) = 2

val () = fun1(x1)
val () = funGT0(x1)

(*
This would produce an unsolved constraint due to
equality constraint:

val () = dubx(x2)

Instead we can do: *)

val () = dubx(#[ 1 | x2])
// ^^^^^^^^^^^^^ This gives the following error
//
// d2exp_trup: loc0 = /home/brandon/witness.dats: 495(line=37, offs=15)
– 505(line=37, offs=25)
// d2exp_trup: d2e0 = D2Eexist(S2EXPARGseq(S2Eintinf(1));
D2Evar(x2$72(-1)))
// /home/brandon/ATS-Postiats/src/pats_trans3_dynexp_up.dats:
12611(line=490, offs=5) – 12621(line=490, offs=15)

}

On Friday, August 15, 2014 11:00:29 PM UTC-4, gmhwxi wrote:

Say you have an expression exp of type int(1).
Say you have a function foo of type Int → void

Note Int = [x:int] int(x).

If you do foo(exp), then the typechecker needs to check
that exp can be given the type Int. In this case, the typechecker
figures out that int(1) can be coerced into Int by setting the witness x
to 1.

Say Int2 = [x:int] int(x*x), and foo2 is of the type Int2 → void.
If you write foo2(exp), the typechecker cannot figure out that int(1) can
be coerced into Int2. Instead, you need to write foo2(#[1 | exp]) (or
foo2(#[~1 | exp])
to indicate to the typechecker that x needs to be set to 1 (or ~1) for
checking
whether int(1) can be coerced into Int2.

On Friday, August 15, 2014 10:12:29 PM UTC-4, Alex Miller wrote:

The syntax #[… | …] allows you to provide witnesses explicitly.

IT COMPILES!!!

I don’t quite understand exactly what #[] means though. I’ve found a
few uses of it throughout doc/, but I can’t seem to find a description
of what the syntax actually means in the ATS book or elsewhere, and I’m
having trouble reasoning it out. Would you mind explaining a bit? How
is this different than providing the type via static/template arguments
(e.g. #[0 | either_left(0)] vs either_left<int 0>(0))?

Dependent types are demanding because handling quantifiers is a lot
harder
than handling propositions (simple types).

I still much prefer writing proofs than tests. I also feel much more
comfortable about my code correctness at the end. :slight_smile:

On Aug 16 2014 at 01:10AM UTC, gmhwxi wrote:

I tidied up the code a bit:

datatype
either_t0ype_bool_type
(
a:t@ype+, b:t@ype+, bool
) =
| Left (a, b, true) of (a)
| Right (a, b, false) of (b)

stadef
either = either_t0ype_bool_type
typedef
either (a:t0p, b:t0p) = [c:bool] either(a, b, c)

fn{
a,b:t0p
} either_left (a:a):<> either(a, b, true) = Left(a)

fn{
a,b:t0p
} either_right (b:b):<> either(a, b, false) = Right(b)

fun do_either(x : int)
: [n:nat; m:nat] either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

implement main0() = ignoret(do_either(~1))

Even a simple example like this would take a lot of effort :slight_smile:

Dependent types are demanding because handling quantifiers is a lot
harder
than handling
propositions (simple types).

On Friday, August 15, 2014 8:58:02 PM UTC-4, gmhwxi wrote:

This one works:

fun do_either(x : int)
: [n:nat; m:nat] Either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 |
either_right(1)]

The syntax #[… | …] allows you to provide witnesses explicitly.

On Friday, August 15, 2014 8:48:25 PM UTC-4, Alex Miller wrote:

The following is a minimal example of a typechecking issue I’ve
been
chasing after for a while. I have an either type that I’ve
implemented,
mimicing the standard library’s option type:

datatype either_t0ype_bool_type
  (a : t@ype+, b : t@ype+, bool) =
    Left (a, b, true) of (a)
  | Right (a, b, false) of (b)
stadef either = either_t0ype_bool_type
typedef Either (a:t0p, b:t0p) = [c : bool] either (a, b, c)

fun{a:t0p}{b:t0p} either_left .<>. (a:a):<> either(a, b, true)

=

Left(a)
fun{a:t0p}{b:t0p} either_right .<>. (b:b):<> either(a, b,
false) =
Right(b)

When I go to use it

fun do_either(x : int) : [n : nat; m : nat] Either (int n, int

m) =

  case+ x of
  | x when x > 0 => either_left(0)
  | x => either_right(1)

implement main0() =
  let
    val _ = do_either(~1)
  in () end

attempts to typecheck this result in

481(line=15, offs=21) -- 511(line=15, offs=51): error(3):

unsolved

constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(7),
S2Eintinf(0)))

I’ve finally understood the reason for this. A call to
either_left
will be able to infer the type for the left side (a) as int 0,
which
satisfies the n >= 0 constraint that nat has. However,
either
still requires a type for the right hand side (b), which has no
constraints put upon it in this case, so the constraint solving
fails
showing that we cannot prove that the type for the right side
satisfies
that the integer will provably be >= 0.

However, I can’t figure out how to solve this. My feeble attempts
to do
either_left<[x:nat] int x>(0) fail, and I feel like there should
be a
clear way to solve this?

14

The syntax #[… | …] allows you to provide witnesses explicitly.

IT COMPILES!!!

I don’t quite understand exactly what #[] means though. I’ve found a
few uses of it throughout doc/, but I can’t seem to find a description
of what the syntax actually means in the ATS book or elsewhere, and I’m
having trouble reasoning it out. Would you mind explaining a bit? How
is this different than providing the type via static/template arguments
(e.g. #[0 | either_left(0)] vs either_left<int 0>(0))?

Dependent types are demanding because handling quantifiers is a lot harder
than handling propositions (simple types).

I still much prefer writing proofs than tests. I also feel much more
comfortable about my code correctness at the end. :)On Aug 16 2014 at 01:10AM UTC, gmhwxi wrote:

I tidied up the code a bit:

datatype
either_t0ype_bool_type
(
a:t@ype+, b:t@ype+, bool
) =
| Left (a, b, true) of (a)
| Right (a, b, false) of (b)

stadef
either = either_t0ype_bool_type
typedef
either (a:t0p, b:t0p) = [c:bool] either(a, b, c)

fn{
a,b:t0p
} either_left (a:a):<> either(a, b, true) = Left(a)

fn{
a,b:t0p
} either_right (b:b):<> either(a, b, false) = Right(b)

fun do_either(x : int)
: [n:nat; m:nat] either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

implement main0() = ignoret(do_either(~1))

Even a simple example like this would take a lot of effort :slight_smile:

Dependent types are demanding because handling quantifiers is a lot harder
than handling
propositions (simple types).

On Friday, August 15, 2014 8:58:02 PM UTC-4, gmhwxi wrote:

This one works:

fun do_either(x : int)
: [n:nat; m:nat] Either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

The syntax #[… | …] allows you to provide witnesses explicitly.

On Friday, August 15, 2014 8:48:25 PM UTC-4, Alex Miller wrote:

The following is a minimal example of a typechecking issue I’ve been
chasing after for a while. I have an either type that I’ve implemented,
mimicing the standard library’s option type:

datatype either_t0ype_bool_type 
  (a : t@ype+, b : t@ype+, bool) = 
    Left (a, b, true) of (a) 
  | Right (a, b, false) of (b) 
stadef either = either_t0ype_bool_type 
typedef Either (a:t0p, b:t0p) = [c : bool] either (a, b, c) 

fun{a:t0p}{b:t0p} either_left .<>. (a:a):<> either(a, b, true) =

Left(a)
fun{a:t0p}{b:t0p} either_right .<>. (b:b):<> either(a, b, false) =
Right(b)

When I go to use it

fun do_either(x : int) : [n : nat; m : nat] Either (int n, int m) = 
  case+ x of 
  | x when x > 0 => either_left(0) 
  | x => either_right(1) 

implement main0() = 
  let 
    val _ = do_either(~1) 
  in () end

attempts to typecheck this result in

481(line=15, offs=21) -- 511(line=15, offs=51): error(3): unsolved

constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(7), S2Eintinf(0)))

I’ve finally understood the reason for this. A call to either_left
will be able to infer the type for the left side (a) as int 0, which
satisfies the n >= 0 constraint that nat has. However, either
still requires a type for the right hand side (b), which has no
constraints put upon it in this case, so the constraint solving fails
showing that we cannot prove that the type for the right side satisfies
that the integer will provably be >= 0.

However, I can’t figure out how to solve this. My feeble attempts to do
either_left<[x:nat] int x>(0) fail, and I feel like there should be a
clear way to solve this?

15

The syntax seems to be slightly different here.

Brandon Barker
brandon…@gmail.comOn Fri, Aug 15, 2014 at 10:27 PM, Brandon Barker brandon...@gmail.com wrote:

I had this same trouble before … more than once. Both instances are
buried deep in this mailing list I think.

I wish you luck in finding them, but perhaps the ATS wiki’s explanation is
good enough (it could probably be improved actually):

Built in operators · githwxi/ATS-Postiats Wiki · GitHub

Brandon Barker
brandon...@gmail.com

On Fri, Aug 15, 2014 at 3:12 PM, Alex Miller mille...@gmail.com wrote:

The syntax #[… | …] allows you to provide witnesses explicitly.

IT COMPILES!!!

I don’t quite understand exactly what #[] means though. I’ve found a
few uses of it throughout doc/, but I can’t seem to find a description
of what the syntax actually means in the ATS book or elsewhere, and I’m
having trouble reasoning it out. Would you mind explaining a bit? How
is this different than providing the type via static/template arguments
(e.g. #[0 | either_left(0)] vs either_left<int 0>(0))?

Dependent types are demanding because handling quantifiers is a lot
harder
than handling propositions (simple types).

I still much prefer writing proofs than tests. I also feel much more
comfortable about my code correctness at the end. :slight_smile:

On Aug 16 2014 at 01:10AM UTC, gmhwxi wrote:

I tidied up the code a bit:

datatype
either_t0ype_bool_type
(
a:t@ype+, b:t@ype+, bool
) =
| Left (a, b, true) of (a)
| Right (a, b, false) of (b)

stadef
either = either_t0ype_bool_type
typedef
either (a:t0p, b:t0p) = [c:bool] either(a, b, c)

fn{
a,b:t0p
} either_left (a:a):<> either(a, b, true) = Left(a)

fn{
a,b:t0p
} either_right (b:b):<> either(a, b, false) = Right(b)

fun do_either(x : int)
: [n:nat; m:nat] either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

implement main0() = ignoret(do_either(~1))

Even a simple example like this would take a lot of effort :slight_smile:

Dependent types are demanding because handling quantifiers is a lot
harder
than handling
propositions (simple types).

On Friday, August 15, 2014 8:58:02 PM UTC-4, gmhwxi wrote:

This one works:

fun do_either(x : int)
: [n:nat; m:nat] Either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

The syntax #[… | …] allows you to provide witnesses explicitly.

On Friday, August 15, 2014 8:48:25 PM UTC-4, Alex Miller wrote:

The following is a minimal example of a typechecking issue I’ve been
chasing after for a while. I have an either type that I’ve
implemented,
mimicing the standard library’s option type:

datatype either_t0ype_bool_type
  (a : t@ype+, b : t@ype+, bool) =
    Left (a, b, true) of (a)
  | Right (a, b, false) of (b)
stadef either = either_t0ype_bool_type
typedef Either (a:t0p, b:t0p) = [c : bool] either (a, b, c)

fun{a:t0p}{b:t0p} either_left .<>. (a:a):<> either(a, b, true) =

Left(a)
fun{a:t0p}{b:t0p} either_right .<>. (b:b):<> either(a, b, false)
=
Right(b)

When I go to use it

fun do_either(x : int) : [n : nat; m : nat] Either (int n, int

m) =

  case+ x of
  | x when x > 0 => either_left(0)
  | x => either_right(1)

implement main0() =
  let
    val _ = do_either(~1)
  in () end

attempts to typecheck this result in

481(line=15, offs=21) -- 511(line=15, offs=51): error(3):

unsolved

constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(7),
S2Eintinf(0)))

I’ve finally understood the reason for this. A call to either_left
will be able to infer the type for the left side (a) as int 0,
which
satisfies the n >= 0 constraint that nat has. However, either
still requires a type for the right hand side (b), which has no
constraints put upon it in this case, so the constraint solving fails
showing that we cannot prove that the type for the right side
satisfies
that the integer will provably be >= 0.

However, I can’t figure out how to solve this. My feeble attempts
to do
either_left<[x:nat] int x>(0) fail, and I feel like there should
be a
clear way to solve this?

–
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/1408128934-sup-4407%40IAmLaptop
.

16

Say you have an expression exp of type int(1).
Say you have a function foo of type Int → void

Note Int = [x:int] int(x).

If you do foo(exp), then the typechecker needs to check
that exp can be given the type Int. In this case, the typechecker
figures out that int(1) can be coerced into Int by setting the witness x to
1.

Say Int2 = [x:int] int(x*x), and foo2 is of the type Int2 → void.
If you write foo2(exp), the typechecker cannot figure out that int(1) can
be coerced into Int2. Instead, you need to write foo2(#[1 | exp]) (or
foo2(#[~1 | exp])
to indicate to the typechecker that x needs to be set to 1 (or ~1) for
checking
whether int(1) can be coerced into Int2.On Friday, August 15, 2014 10:12:29 PM UTC-4, Alex Miller wrote:

The syntax #[… | …] allows you to provide witnesses explicitly.

IT COMPILES!!!

I don’t quite understand exactly what #[] means though. I’ve found a
few uses of it throughout doc/, but I can’t seem to find a description
of what the syntax actually means in the ATS book or elsewhere, and I’m
having trouble reasoning it out. Would you mind explaining a bit? How
is this different than providing the type via static/template arguments
(e.g. #[0 | either_left(0)] vs either_left<int 0>(0))?

Dependent types are demanding because handling quantifiers is a lot
harder
than handling propositions (simple types).

I still much prefer writing proofs than tests. I also feel much more
comfortable about my code correctness at the end. :slight_smile:

On Aug 16 2014 at 01:10AM UTC, gmhwxi wrote:

I tidied up the code a bit:

datatype
either_t0ype_bool_type
(
a:t@ype+, b:t@ype+, bool
) =
| Left (a, b, true) of (a)
| Right (a, b, false) of (b)

stadef
either = either_t0ype_bool_type
typedef
either (a:t0p, b:t0p) = [c:bool] either(a, b, c)

fn{
a,b:t0p
} either_left (a:a):<> either(a, b, true) = Left(a)

fn{
a,b:t0p
} either_right (b:b):<> either(a, b, false) = Right(b)

fun do_either(x : int)
: [n:nat; m:nat] either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

implement main0() = ignoret(do_either(~1))

Even a simple example like this would take a lot of effort :slight_smile:

Dependent types are demanding because handling quantifiers is a lot
harder
than handling
propositions (simple types).

On Friday, August 15, 2014 8:58:02 PM UTC-4, gmhwxi wrote:

This one works:

fun do_either(x : int)
: [n:nat; m:nat] Either (int n, int m) =
if x > 0 then #[0,1 | either_left(0)] else #[0,1 | either_right(1)]

The syntax #[… | …] allows you to provide witnesses explicitly.

On Friday, August 15, 2014 8:48:25 PM UTC-4, Alex Miller wrote:

The following is a minimal example of a typechecking issue I’ve been
chasing after for a while. I have an either type that I’ve
implemented,
mimicing the standard library’s option type:

datatype either_t0ype_bool_type 
  (a : t@ype+, b : t@ype+, bool) = 
    Left (a, b, true) of (a) 
  | Right (a, b, false) of (b) 
stadef either = either_t0ype_bool_type 
typedef Either (a:t0p, b:t0p) = [c : bool] either (a, b, c) 

fun{a:t0p}{b:t0p} either_left .<>. (a:a):<> either(a, b, true) =

Left(a)
fun{a:t0p}{b:t0p} either_right .<>. (b:b):<> either(a, b, false)
=
Right(b)

When I go to use it

fun do_either(x : int) : [n : nat; m : nat] Either (int n, int m)

=

  case+ x of 
  | x when x > 0 => either_left(0) 
  | x => either_right(1) 

implement main0() = 
  let 
    val _ = do_either(~1) 
  in () end

attempts to typecheck this result in

481(line=15, offs=21) -- 511(line=15, offs=51): error(3):

unsolved

constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(7),
S2Eintinf(0)))

I’ve finally understood the reason for this. A call to either_left
will be able to infer the type for the left side (a) as int 0,
which
satisfies the n >= 0 constraint that nat has. However, either
still requires a type for the right hand side (b), which has no
constraints put upon it in this case, so the constraint solving fails
showing that we cannot prove that the type for the right side
satisfies
that the integer will provably be >= 0.

However, I can’t figure out how to solve this. My feeble attempts to
do
either_left<[x:nat] int x>(0) fail, and I feel like there should be
a
clear way to solve this?