Constraining unspecified types

[Alex Miller]

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?

[gmhwxi]

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.

[gmhwxi]

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

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

[Alex Miller]

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

[Brandon Barker]

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

https://github.com/githwxi/ATS-Postiats/wiki/Built-in-operators

Brandon Barker
brandon...@gmail.com

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

[Brandon Barker]

The syntax seems to be slightly different here.

Brandon Barker
brandon...@gmail.com

[gmhwxi]

#[...] and #[... | ...] are unrelated syntax.

[gmhwxi]

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.

[gmhwxi]

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)

[Brandon Barker]

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(2*x)
typedef Int2 = [x:int] int(x*x)




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)



}

[Brandon Barker]

(But, the working either example posted above does typecheck for me.)

[Alex Miller]

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" ?

[Brandon Barker]

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

Brandon Barker
brandon...@gmail.com

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

[gmhwxi]

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:

[Hongwei Xi]

>>Thanks for pointing out the bug.

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

[Brandon Barker]

Great, I added clarifications for operators here  and linked to both examples on the typechecking errors page (also included some other recent examples/discussion there).

Brandon Barker
brandon...@gmail.com

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