Difficulties getting equality working with higher-kinded types

[vamc...@gmail.com]

Hi all,

I have been trying to implement something like Haskell's Data.Either module in ATS. I'd like to be able to test equality generically. This is my .sats file:

#include "share/atspre_staload_libats_ML.hats"
#include "libats/ML/SATS/SHARE/monad.hats"

datatype either(a: t@ype, b: t@ype+) =
  | left of a
  | right of b

fun eq_either_either {a:t@ype}{b:t@ype+} (x : either(a, b), y : either(a, b)) : bool

fun neq_either_either {a:t@ype}{b:t@ype+} (x : either(a, b), y : either(a, b)) : bool

overload = with eq_either_either

overload != with neq_either_either

fun lefts {a:t@ype}{b:t@ype+}{n:int} (x : list(either(a,b), n)) :
  [ m : int | m <= n ] list(a, m)

fun rights {a:t@ype}{b:t@ype+}{n:int} (x : list(either(a,b), n)) :
  [ m : int | m <= n ] list(b, m)

fun either_ {a:t@ype}{b:t@ype+}{c:t@ype} (f : a -> c, g : b -> c, x : either(a, b)) : c

fun is_left {a:t@ype}{b:t@ype+} (x : either(a, b)) : bool

fun is_right {a:t@ype}{b:t@ype+} (x : either(a, b)) : bool

fun from_right {a:t@ype}{b:t@ype+} (x : b, y : either(a, b)) : b

fun from_left {a:t@ype}{b:t@ype+} (x : a, y : either(a, b)) : a

and this is my .dats file:

staload "either.sats"
staload "prelude/SATS/list.sats"

#include "prelude/DATS/basics.dats"
#include "prelude/DATS/list.dats"

assume monad_type(b : t0p) = [a:t0p] either(a, b)

implement eq_either_either (x, y) =
  case+ (x, y) of
    | (right (_), left (_)) => false
    | (left (_), right (_)) => false
    | (left (x), left (y)) => gequal_val_val(x, y)
    | (right (x), right (y)) => gequal_val_val(x, y)

implement neq_either_either (x, y) =
  not(eq_either_either(x, y))

datasort list =
  | NIL
  | CONS of list

dataprop LENGTH(list, int) =
  | L_NIL(NIL, 0)
  | {l:list}{len:nat} L_CONS(CONS(l), 1 + len) of (LENGTH(l, len))

implement lefts (ys) =
  case- ys of
    | list_nil() => list_nil()
    | list_cons (right (x), xs) => lefts(xs)

// | list_cons (left (x), xs) => list_cons(x, lefts(xs))
// functorial proof functions?
// want to prove: if length(f(xs)) <= n, length(xs) = n, length(cons(x, xs)) <= length(cons(x, f(xs)))
implement {a} monad_return (x) =
  right(x)

implement {a} monad_join (x) =
  case+ x of
    | left (y) => left(y)
    | right (left (y)) => left(y)
    | right (right (x)) => right(x)

implement {a}{b} monad_fmap (fopr, x) =
  case+ x of
    | left (y) => left(y)
    | right (x) => right(fopr(x))

implement {a}{b} monad_bind (x, fopr) =
  case+ x of
    | left (y) => left(y)
    | right (y) => fopr(y)

my .hats file:

staload "./either.sats"
staload _ = "./either.dats"

and finally the actual test suite:

#include "share/atspre_staload.hats"
#include "share/atspre_staload_libats_ML.hats"
#include "either.hats"

staload "prelude/SATS/tostring.sats"
staload "libats/ML/SATS/string.sats"

#define nil list_vt_nil

#define :: list_vt_cons

fn test_eq1() : bool =
  let
    val rhs: either(string, string) = right("eq")
    val lhs: either(string, string) = right("eq")
  in
    rhs = lhs
  end

fn test_eq2() : bool =
  true

vtypedef named = @{ fst = string, snd = bool }
vtypedef test_tree = @{ group = string, leaves = List_vt(named) }

fn fail_incomplete(i : int, n : int) : void =
  {
    val _ = prerr!("\nTest suite complete (" + tostring_int(i) + "/" + tostring_int(n) + ")\n")
    val _ = if n != i then
      (exit(1) ; ())
    else
      ()
  }

fnx iterate_list(t : test_tree, i : int, n : int) : void =
  let
    val _ = if i = 0 then
      println!(t.group + ":")
    else
      ()
   
    fun handle_loop(s : string, b : bool, xs : test_tree) : void =
      if b then
        (println!("  \33[32msucceeded:\33[0m " + s) ; iterate_list(xs, i + 1, n))
      else
        (println!("  \33[31mfailed:\33[0m " + s) ; iterate_list(xs, i, n))
  in
    case+ t.leaves of
      | ~list_vt_nil() => fail_incomplete(i, n)
      | ~list_vt_cons (x, xs) => handle_loop(x.fst, x.snd, @{ group = t.group, leaves = xs })
  end

implement main0 () =
  {
    var n0 = @{ fst = "eq (1/2)", snd = test_eq1() }
    var n1 = @{ fst = "eq (2/2)", snd = test_eq2() }
    var xs = n0 :: n1 :: nil
    var total = list_vt_length(xs)
    val g = @{ group = "monad_join", leaves = xs } : test_tree
    val _ = iterate_list(g, 0, total)
  }

which fails to build with the following error:

/tmp/ccrn6Wjd.o: In function `mainats_void_0': test_dats.c:(.text+0x391): undefined reference to `_057_home_057_vanessa_057__056_atspkg_057_0_056_3_056_9_057_lib_057_ats2_055_postiats_055_0_056_3_056_9_057_either_056_sats__eq_either_either' collect2: error: ld returned 1 exit status )

Am I doing something wrong here? I tried to get generic equality on lists working as well, but I couldn't seem to figure out how. I tried this with ATS 0.3.9 as well as ATS 0.3.10. Any insight would be much appreciated!

Thanks!

[vamc...@gmail.com]

Also, the full source code is here: http://github.com/vmchale/either

This might occlude some relevant bits since it uses atspkg but hopefully not?

[gmhwxi]

There are several issues here.

First, eq and neq should be function templates (rather than polymorphic functions):

datatype either(a: t@ype, b: t@ype+) =
  | left of a
  | right of b

fun

{a:t@ype}
{b:t@ype}
eq_either_either(x : either(a, INV(b)), y : either(a, b)) : bool

fun
{a:t@ype}
{b:t@ype}
neq_either_either(x : either(a, INV(b)), y : either(a, b)) : bool

overload = with eq_either_either

overload != with neq_either_either

Since the second argument of 'either' is declared to be co-variant, INV(b) is used in the interface for eq and neq
to make overloading of = and != work.

The function of test_eq1 needs to be modified slightly:

fn test_eq1() : bool =
    let
      val rhs = right{string,string}("eq")
      val lhs = right{string,string}("eq")

    in
      rhs = lhs
    end

If you write rhs:either(string, string) = right("eq"), then the typechecker only knows that the type assigned to rhs is either(string, X) for some X <= string.

Now your code can be compiled to an executable. I saw the following when trying it:

monad_join:
  succeeded: eq (1/2)
  succeeded: eq (2/2)

Test suite complete (2/2)

A more serious issue with your code is the following one:

assume monad_type(b : t0p) = [a:t0p] either(a, b)

This is unlikely to work. I think what you need is monad(a, b) where 'a' serves
as a parameter:

abstype monad_type(a: t@ype, b:t@ype)
assume monad_type(a:t0p, b:t0p) = either(a, b)

On Sunday, February 11, 2018 at 8:27:15 PM UTC-5

[gmhwxi]

Forgot to paste the code for 'eq' that I used:

implement
{a}{b}

eq_either_either (x, y) =
  case+ (x, y) of
    | (right (_), left (_)) => false
    | (left (_), right (_)) => false

    | (left (x), left (y)) => gequal_val_val<a>(x, y)
    | (right (x), right (y)) => gequal_val_val<b>(x, y)

[vamc...@gmail.com]

Great, thanks for the reply! I'll have a look at updating it soon.