Re: [ats-lang-users] Constraints in an 'if'

[Guillaume B. <gui...@en...>]

2009/12/10 Hongwei Xi <hw...@cs...>

> On Thu, 10 Dec 2009, Guillaume Brunerie wrote:
>
> >>Hi, I know ATS just for a few days, and wanted to do some experiments.
> >>I wrote the following functions :
> >>
> >>
> >>
> >>datatype list (a:t@ype+, int) = // polymorphic datatype
> >>  | nil (a, 0)
> >>  | {n:nat} cons (a, n+1) of (a, list (a, n))
> >>
> >>fun{a1,a2:t@ype} {n:nat} zip_list
> >>  (xs1: list (a1, n), xs2: list (a2, n)): list ('(a1, a2), n) =
> >>  case+ (xs1, xs2) of
> >>  | (cons (x1, xs1), cons (x2, xs2)) => cons ('(x1, x2), zip_list (xs1,
> >>xs2))
> >>  | (nil (), nil ()) => nil ()
> >>
> >>fun {n : nat} f1 (l1 : list(int, n), l2 : list(int, n)) =
> >>    zip_list (l1, l2)
>
> By the way, it should be written as
>
> fun f1 {n:nat} (l1: list(int, n), l2: list (int, n)) = ...
>
> Otherwise, you will have a problem when using the function.



What are the differences ? And why shouldn’t not also zipwith be written
like that ?
I thought that writing the universal quantifier before or after the name of
the function was irrelevant.



> >>fun {n : nat} f2 (l1 : list(int, n), l2 : list(int, n)) =
> >>  if 0 = 0 then
> >>    zip_list (l1, l2)
> >>  else
> >>    zip_list (l1, l2)
>
> >>The function f1 is correctly typechecked, but not the function f2, the
> typer
> >>saying that there are unsolved constraints.
> >>Why? How can I tell the typechecker that the two lists actually have the
> >>same length.
>
> The type of the return value of f2 should be given as well:
>
> fun f2 {n:nat} (l1 : list(int, n), l2 : list(int, n))
>  : list ('(int,int), n) = ...



Yes, sorry, I completely forgot to give the type of the return value of the
function. Now it compiles correctly, thank you.



> >>BTW, is it normal that the error messages I get look like this :
> >>error(3): unsolved constraint: C3STRprop(none; S2Etyleq(0;
> >>S2Eapp(S2Ecst(list); S2Etyrec(box; 0; 0=S2EVar(20), 1=S2EVar(21)),
> >>S2EVar(22)), S2EVar(17)))
> >>s3bexp_make_s2exp: s2e0 = S2Etyleq(0; S2Eapp(S2Ecst(list); S2Etyrec(box;
> 0;
> >>0=S2EVar(23), 1=S2EVar(24)), S2EVar(25)), S2EVar(17))
> >>?
> >>It is not very easy to read...
>
> True. Dependent type-checking is messy. Normally, you don't need to read
> such messages. What you really need is the location of the error.
>
> --Hongwei
>
> Computer Science Department
> Boston University
> 111 Cummington Street
> Boston, MA 02215
>
> Email: hw...@cs...
> Url: http://www.cs.bu.edu/~hwxi
> Tel: +1 617 358 2511 (office)
> Fax: +1 617 353 6457 (department)
>

Guillaume Brunerie