Higher Kinds in ATS and More monads questions

Google Group
1

I have not read fully the link given previously on monad. So please ignore
if it is duplicate code of it . (some I copied,other I ignored temporary
for now )

Monad part 1 :

#include “share/atspre_define.hats”
#include “share/atspre_staload.hats”

datatype Maybe (a : t@ype) =
| Nothing (a) of ()
| Just (a) of (a)

abstype M (t@ype) = ptr

extern
fun{a:t@ype} ret : a -> M (a)

typedef cfun (a:t@ype,b:t@ype) = a - M (b)

extern
fun{a,b:t@ype} bind : (M (a) , cfun (a, b)) -> M (b)

assume M (a : t@ype) = Maybe (a)

implement{a}
ret (x) = Just (x)

implement{a,b}
bind (m , f) =
case m of
| Nothing _ => Nothing
| Just (x) => f (x)

fun (* {a:t@ype} *)
print_maybe (ma : Maybe (int)) : void =
case ma of
| Nothing _ => println! (“Nothing”)
| Just (x) => println! (x)

datatype Expr =
| Val of Int
| Div of (Expr , Expr)

val ok = Div (Div ( Val (1972) , Val (2) ) , Val (23))

(* val err = Div (Val 2) (Div (Val 1) (Div (Val 2) (Val 3))) *)
val err = Div (Val (2) , Div (Val (1) , Div (Val (2) , Val (3))))

extern
fun div (m : int , n : int) : Maybe(int)

fun eval (e : Expr) : Maybe(int) =
case e of
| Val n => ret (n)
| Div (e1 , e2) =>
bind<int,int> (eval e1 ,
(lam m =>
bind<int,int> (eval e2,
(lam n => div (m,n)))))

implement
div (m , n) =
if n = 0
then Nothing ()
else ret (m / n)

datatype Opt (a:t@ype) =
| None of ()
| Some (a) of (a)

//assume M (a : t@ype) = Opt (a)

implement main0 () = () where {
val _ = println! (“Monad”)
val res1 = eval ok
val res2 = eval err
val _ = print_maybe (res1)
val _ = print_maybe (res2)

}

So now I can use monadic computation in ATS , but cannot use two different
monads in same program, for example I can use Maybe monad but not Opt
in given above code (right ?)

Maybe above is a higher kind or a type constructor : (t@ype -> type)
(right ?) .

So why not implement monads as given below

Monad Part 2 :

#include “share/atspre_define.hats”
#include “share/atspre_staload.hats”

datatype Maybe (a : t@ype) =
| Nothing (a) of ()
| Just (a) of (a)

typedef cfun (M:(t@ype -> type), a:t@ype,b:t@ype) = a - M (b)

extern
fun{a:t@ype}{H : (t@ype -> type)}
ret : a -> H (a)

extern
fun {a,b:t@ype}{H : (t@ype -> type)}
bind: (H (a) , cfun (H,a,b)) -> H (b)

implement(a)
ret (x) = Just (x)

implement(a,b)
bind<a,b> (ma , f) =
case ma of
| Nothing _ => Nothing
| Just (x) => f (x)

datatype Expr =
| Val of Int
| Div of (Expr , Expr)

val ok = Div (Div ( Val (1972) , Val (2) ) , Val (23))

val err = Div (Val (2) , Div (Val (1) , Div (Val (2) , Val (3))))

extern
fun div (m : int , n : int) : Maybe(int)

fun eval (e : Expr) : Maybe(int) =
case e of
| Val n => ret (n)
| Div (e1 , e2) =>
bind<int,int> (eval e1 ,
(lam m =>
bind<int,int> (eval e2,
(lam n => div (m,n)))))

implement
div (m , n) =
if n = 0
then Nothing ()
else ret (m / n)

fun (* {a:t@ype} *)
print_maybe (ma : Maybe (int)) : void =
case ma of
| Nothing _ => println! (“Nothing”)
| Just (x) => println! (x)

datatype Opt (a:t@ype) =
| None of ()
| Some (a) of (a)

implement(a)
ret (x) = Some (x)

implement(a,b)
bind<a,b> (ma , f) =
case ma of
| None _ => None
| Some (x) => f (x)

fun (* {a:t@ype} *)
print_opt (opt : Opt (int)) : void =
case opt of
| None _ => println! (“None”)
| Some (x) => println! (x)

implement main0 () = () where {
val _ = println! (“Monads”)
val mi = ret (100)
val _ = print_maybe (mi)
val res1 = eval ok
val res2 = eval err

val _ = print_maybe (res1)
val _ = print_maybe (res2)

val _ = print_opt (ret (1000))
}

Above code runs without any error.

Now I can use both Opt and Maybe in same program.

Is the above code correct and what does it mean to have (t@ype -> type) in
template arguments.

Thanks.

2

I would like to show a bit here that the syntax of ATS can actually support
the use of monads
reasonably well.

See:

for the following code:

//
datatype expr =
| Val of Int
| Div of (expr, expr)
//
(* ****** ****** )
//
macdef non() = monad_maybe_none()
//
macdef ret(x) = monad_return (,(x))
//
infix >>=
macdef >>= (x, f) = monad_bind (,(x), ,(f))
//
( ****** ****** *)

fun
idiv
(
i1: int, i2: int
) : monad(int) = if i2 != 0 then ret(i1/i2) else non()

(* ****** ****** *)

fun
eval(x0: expr): monad(int) =
(
case+ x0 of
| Val(i) => ret(i)
| Div(x1, x2) =>
eval(x1) >>= (lam i1 => eval(x2) >>= (lam i2 => idiv(i1, i2)))
) (* end of [eval] *)

(* ****** ****** )
//
macdef V_(x) = Val(,(x))
//
fun{}
Div_(x: expr, y: expr): expr = Div(x, y)
//
overload / with Div_
//
val ok = V_(1972) / V_(2) / V_(23)
val err = V_(2) / ( V_(1) / (V_(2) / V_(3)))
//
val () = fprintln! (stdout_ref, "eval(ok) = ", eval(ok))
val () = fprintln! (stdout_ref, "eval(err) = ", eval(err))
//
( ****** ****** *)On Saturday, April 4, 2015 at 8:18:45 AM UTC-4, gmhwxi wrote:

There are currently list-monad and maybe-monad available in ATSLIB:

https://github.com/githwxi/ATS-Postiats/blob/master/libats/ML/SATS/monad_list.sats

https://github.com/githwxi/ATS-Postiats/blob/master/libats/ML/SATS/monad_maybe.sats

Higher-order template parameters are an experimental feature. There is
currently no documentation
for it.

Your monad implementation is of Haskell style (type class). For using
monads in ATS, I feel that ML
style (module) is likely to be more convenient.

On Saturday, April 4, 2015 at 5:18:10 AM UTC-4, Chotu S wrote:

I have not read fully the link given previously on monad. So please
ignore if it is duplicate code of it . (some I copied,other I ignored
temporary for now )

Monad part 1 :

#include “share/atspre_define.hats”
#include “share/atspre_staload.hats”

datatype Maybe (a : t@ype) =
| Nothing (a) of ()
| Just (a) of (a)

abstype M (t@ype) = ptr

extern
fun{a:t@ype} ret : a → M (a)

typedef cfun (a:t@ype,b:t@ype) = a - M (b)

extern
fun{a,b:t@ype} bind : (M (a) , cfun (a, b)) → M (b)

assume M (a : t@ype) = Maybe (a)

implement{a}
ret (x) = Just (x)

implement{a,b}
bind (m , f) =
case m of
| Nothing _ => Nothing
| Just (x) => f (x)

fun (* {a:t@ype} *)
print_maybe (ma : Maybe (int)) : void =
case ma of
| Nothing _ => println! (“Nothing”)
| Just (x) => println! (x)

datatype Expr =
| Val of Int
| Div of (Expr , Expr)

val ok = Div (Div ( Val (1972) , Val (2) ) , Val (23))

(* val err = Div (Val 2) (Div (Val 1) (Div (Val 2) (Val 3))) *)
val err = Div (Val (2) , Div (Val (1) , Div (Val (2) , Val (3))))

extern
fun div (m : int , n : int) : Maybe(int)

fun eval (e : Expr) : Maybe(int) =
case e of
| Val n => ret (n)
| Div (e1 , e2) =>
bind<int,int> (eval e1 ,
(lam m =>
bind<int,int> (eval e2,
(lam n => div (m,n)))))

implement
div (m , n) =
if n = 0
then Nothing ()
else ret (m / n)

datatype Opt (a:t@ype) =
| None of ()
| Some (a) of (a)

//assume M (a : t@ype) = Opt (a)

implement main0 () = () where {
val _ = println! (“Monad”)
val res1 = eval ok
val res2 = eval err
val _ = print_maybe (res1)
val _ = print_maybe (res2)

}

So now I can use monadic computation in ATS , but cannot use two
different monads in same program, for example I can use Maybe monad but
not Opt in given above code (right ?)

Maybe above is a higher kind or a type constructor : (t@ype → type)
(right ?) .

So why not implement monads as given below

Monad Part 2 :

#include “share/atspre_define.hats”
#include “share/atspre_staload.hats”

datatype Maybe (a : t@ype) =
| Nothing (a) of ()
| Just (a) of (a)

typedef cfun (M:(t@ype → type), a:t@ype,b:t@ype) = a - M (b)

extern
fun{a:t@ype}{H : (t@ype → type)}
ret : a → H (a)

extern
fun {a,b:t@ype}{H : (t@ype → type)}
bind: (H (a) , cfun (H,a,b)) → H (b)

implement(a)
ret (x) = Just (x)

implement(a,b)
bind<a,b> (ma , f) =
case ma of
| Nothing _ => Nothing
| Just (x) => f (x)

datatype Expr =
| Val of Int
| Div of (Expr , Expr)

val ok = Div (Div ( Val (1972) , Val (2) ) , Val (23))

val err = Div (Val (2) , Div (Val (1) , Div (Val (2) , Val (3))))

extern
fun div (m : int , n : int) : Maybe(int)

fun eval (e : Expr) : Maybe(int) =
case e of
| Val n => ret (n)
| Div (e1 , e2) =>
bind<int,int> (eval e1 ,
(lam m =>
bind<int,int> (eval e2,
(lam n => div (m,n)))))

implement
div (m , n) =
if n = 0
then Nothing ()
else ret (m / n)

fun (* {a:t@ype} *)
print_maybe (ma : Maybe (int)) : void =
case ma of
| Nothing _ => println! (“Nothing”)
| Just (x) => println! (x)

datatype Opt (a:t@ype) =
| None of ()
| Some (a) of (a)

implement(a)
ret (x) = Some (x)

implement(a,b)
bind<a,b> (ma , f) =
case ma of
| None _ => None
| Some (x) => f (x)

fun (* {a:t@ype} *)
print_opt (opt : Opt (int)) : void =
case opt of
| None _ => println! (“None”)
| Some (x) => println! (x)

implement main0 () = () where {
val _ = println! (“Monads”)
val mi = ret (100)
val _ = print_maybe (mi)
val res1 = eval ok
val res2 = eval err

val _ = print_maybe (res1)
val _ = print_maybe (res2)

val _ = print_opt (ret (1000))
}

Above code runs without any error.

Now I can use both Opt and Maybe in same program.

Is the above code correct and what does it mean to have (t@ype → type)
in template arguments.

Thanks.

3

I have been working through some first time haskell tutorials and was
impressed by the power of monad there , so wanted to see if I can implement
monad in ATS as it seems to simplify lots of computation patterns.

I hope this higher order template parameters facility will remain or
available in future , looks interesting to me .

I’ll study examples you have given soon.

Thanks.On Saturday, April 4, 2015 at 5:48:45 PM UTC+5:30, gmhwxi wrote:

There are currently list-monad and maybe-monad available in ATSLIB:

https://github.com/githwxi/ATS-Postiats/blob/master/libats/ML/SATS/monad_list.sats

https://github.com/githwxi/ATS-Postiats/blob/master/libats/ML/SATS/monad_maybe.sats

Higher-order template parameters are an experimental feature. There is
currently no documentation
for it.

Your monad implementation is of Haskell style (type class). For using
monads in ATS, I feel that ML
style (module) is likely to be more convenient.

On Saturday, April 4, 2015 at 5:18:10 AM UTC-4, Chotu S wrote:

I have not read fully the link given previously on monad. So please
ignore if it is duplicate code of it . (some I copied,other I ignored
temporary for now )

Monad part 1 :

#include “share/atspre_define.hats”
#include “share/atspre_staload.hats”

datatype Maybe (a : t@ype) =
| Nothing (a) of ()
| Just (a) of (a)

abstype M (t@ype) = ptr

extern
fun{a:t@ype} ret : a → M (a)

typedef cfun (a:t@ype,b:t@ype) = a - M (b)

extern
fun{a,b:t@ype} bind : (M (a) , cfun (a, b)) → M (b)

assume M (a : t@ype) = Maybe (a)

implement{a}
ret (x) = Just (x)

implement{a,b}
bind (m , f) =
case m of
| Nothing _ => Nothing
| Just (x) => f (x)

fun (* {a:t@ype} *)
print_maybe (ma : Maybe (int)) : void =
case ma of
| Nothing _ => println! (“Nothing”)
| Just (x) => println! (x)

datatype Expr =
| Val of Int
| Div of (Expr , Expr)

val ok = Div (Div ( Val (1972) , Val (2) ) , Val (23))

(* val err = Div (Val 2) (Div (Val 1) (Div (Val 2) (Val 3))) *)
val err = Div (Val (2) , Div (Val (1) , Div (Val (2) , Val (3))))

extern
fun div (m : int , n : int) : Maybe(int)

fun eval (e : Expr) : Maybe(int) =
case e of
| Val n => ret (n)
| Div (e1 , e2) =>
bind<int,int> (eval e1 ,
(lam m =>
bind<int,int> (eval e2,
(lam n => div (m,n)))))

implement
div (m , n) =
if n = 0
then Nothing ()
else ret (m / n)

datatype Opt (a:t@ype) =
| None of ()
| Some (a) of (a)

//assume M (a : t@ype) = Opt (a)

implement main0 () = () where {
val _ = println! (“Monad”)
val res1 = eval ok
val res2 = eval err
val _ = print_maybe (res1)
val _ = print_maybe (res2)

}

So now I can use monadic computation in ATS , but cannot use two
different monads in same program, for example I can use Maybe monad but
not Opt in given above code (right ?)

Maybe above is a higher kind or a type constructor : (t@ype → type)
(right ?) .

So why not implement monads as given below

Monad Part 2 :

#include “share/atspre_define.hats”
#include “share/atspre_staload.hats”

datatype Maybe (a : t@ype) =
| Nothing (a) of ()
| Just (a) of (a)

typedef cfun (M:(t@ype → type), a:t@ype,b:t@ype) = a - M (b)

extern
fun{a:t@ype}{H : (t@ype → type)}
ret : a → H (a)

extern
fun {a,b:t@ype}{H : (t@ype → type)}
bind: (H (a) , cfun (H,a,b)) → H (b)

implement(a)
ret (x) = Just (x)

implement(a,b)
bind<a,b> (ma , f) =
case ma of
| Nothing _ => Nothing
| Just (x) => f (x)

datatype Expr =
| Val of Int
| Div of (Expr , Expr)

val ok = Div (Div ( Val (1972) , Val (2) ) , Val (23))

val err = Div (Val (2) , Div (Val (1) , Div (Val (2) , Val (3))))

extern
fun div (m : int , n : int) : Maybe(int)

fun eval (e : Expr) : Maybe(int) =
case e of
| Val n => ret (n)
| Div (e1 , e2) =>
bind<int,int> (eval e1 ,
(lam m =>
bind<int,int> (eval e2,
(lam n => div (m,n)))))

implement
div (m , n) =
if n = 0
then Nothing ()
else ret (m / n)

fun (* {a:t@ype} *)
print_maybe (ma : Maybe (int)) : void =
case ma of
| Nothing _ => println! (“Nothing”)
| Just (x) => println! (x)

datatype Opt (a:t@ype) =
| None of ()
| Some (a) of (a)

implement(a)
ret (x) = Some (x)

implement(a,b)
bind<a,b> (ma , f) =
case ma of
| None _ => None
| Some (x) => f (x)

fun (* {a:t@ype} *)
print_opt (opt : Opt (int)) : void =
case opt of
| None _ => println! (“None”)
| Some (x) => println! (x)

implement main0 () = () where {
val _ = println! (“Monads”)
val mi = ret (100)
val _ = print_maybe (mi)
val res1 = eval ok
val res2 = eval err

val _ = print_maybe (res1)
val _ = print_maybe (res2)

val _ = print_opt (ret (1000))
}

Above code runs without any error.

Now I can use both Opt and Maybe in same program.

Is the above code correct and what does it mean to have (t@ype → type)
in template arguments.

Thanks.

4

There are currently list-monad and maybe-monad available in ATSLIB:

Higher-order template parameters are an experimental feature. There is
currently no documentation
for it.

Your monad implementation is of Haskell style (type class). For using
monads in ATS, I feel that ML
style (module) is likely to be more convenient.On Saturday, April 4, 2015 at 5:18:10 AM UTC-4, Chotu S wrote:

I have not read fully the link given previously on monad. So please ignore
if it is duplicate code of it . (some I copied,other I ignored temporary
for now )

Monad part 1 :

#include “share/atspre_define.hats”
#include “share/atspre_staload.hats”

datatype Maybe (a : t@ype) =
| Nothing (a) of ()
| Just (a) of (a)

abstype M (t@ype) = ptr

extern
fun{a:t@ype} ret : a → M (a)

typedef cfun (a:t@ype,b:t@ype) = a - M (b)

extern
fun{a,b:t@ype} bind : (M (a) , cfun (a, b)) → M (b)

assume M (a : t@ype) = Maybe (a)

implement{a}
ret (x) = Just (x)

implement{a,b}
bind (m , f) =
case m of
| Nothing _ => Nothing
| Just (x) => f (x)

fun (* {a:t@ype} *)
print_maybe (ma : Maybe (int)) : void =
case ma of
| Nothing _ => println! (“Nothing”)
| Just (x) => println! (x)

datatype Expr =
| Val of Int
| Div of (Expr , Expr)

val ok = Div (Div ( Val (1972) , Val (2) ) , Val (23))

(* val err = Div (Val 2) (Div (Val 1) (Div (Val 2) (Val 3))) *)
val err = Div (Val (2) , Div (Val (1) , Div (Val (2) , Val (3))))

extern
fun div (m : int , n : int) : Maybe(int)

fun eval (e : Expr) : Maybe(int) =
case e of
| Val n => ret (n)
| Div (e1 , e2) =>
bind<int,int> (eval e1 ,
(lam m =>
bind<int,int> (eval e2,
(lam n => div (m,n)))))

implement
div (m , n) =
if n = 0
then Nothing ()
else ret (m / n)

datatype Opt (a:t@ype) =
| None of ()
| Some (a) of (a)

//assume M (a : t@ype) = Opt (a)

implement main0 () = () where {
val _ = println! (“Monad”)
val res1 = eval ok
val res2 = eval err
val _ = print_maybe (res1)
val _ = print_maybe (res2)

}

So now I can use monadic computation in ATS , but cannot use two different
monads in same program, for example I can use Maybe monad but not Opt
in given above code (right ?)

Maybe above is a higher kind or a type constructor : (t@ype → type)
(right ?) .

So why not implement monads as given below

Monad Part 2 :

#include “share/atspre_define.hats”
#include “share/atspre_staload.hats”

datatype Maybe (a : t@ype) =
| Nothing (a) of ()
| Just (a) of (a)

typedef cfun (M:(t@ype → type), a:t@ype,b:t@ype) = a - M (b)

extern
fun{a:t@ype}{H : (t@ype → type)}
ret : a → H (a)

extern
fun {a,b:t@ype}{H : (t@ype → type)}
bind: (H (a) , cfun (H,a,b)) → H (b)

implement(a)
ret (x) = Just (x)

implement(a,b)
bind<a,b> (ma , f) =
case ma of
| Nothing _ => Nothing
| Just (x) => f (x)

datatype Expr =
| Val of Int
| Div of (Expr , Expr)

val ok = Div (Div ( Val (1972) , Val (2) ) , Val (23))

val err = Div (Val (2) , Div (Val (1) , Div (Val (2) , Val (3))))

extern
fun div (m : int , n : int) : Maybe(int)

fun eval (e : Expr) : Maybe(int) =
case e of
| Val n => ret (n)
| Div (e1 , e2) =>
bind<int,int> (eval e1 ,
(lam m =>
bind<int,int> (eval e2,
(lam n => div (m,n)))))

implement
div (m , n) =
if n = 0
then Nothing ()
else ret (m / n)

fun (* {a:t@ype} *)
print_maybe (ma : Maybe (int)) : void =
case ma of
| Nothing _ => println! (“Nothing”)
| Just (x) => println! (x)

datatype Opt (a:t@ype) =
| None of ()
| Some (a) of (a)

implement(a)
ret (x) = Some (x)

implement(a,b)
bind<a,b> (ma , f) =
case ma of
| None _ => None
| Some (x) => f (x)

fun (* {a:t@ype} *)
print_opt (opt : Opt (int)) : void =
case opt of
| None _ => println! (“None”)
| Some (x) => println! (x)

implement main0 () = () where {
val _ = println! (“Monads”)
val mi = ret (100)
val _ = print_maybe (mi)
val res1 = eval ok
val res2 = eval err

val _ = print_maybe (res1)
val _ = print_maybe (res2)

val _ = print_opt (ret (1000))
}

Above code runs without any error.

Now I can use both Opt and Maybe in same program.

Is the above code correct and what does it mean to have (t@ype → type) in
template arguments.

Thanks.