Some monads without higher-order functions

Here’s something a came up with:

This shows a Maybe monad from Haskell in ATS/Postiats. The idea is that no
higher-order functions are involved (and no closures too). If it works,
then it means we have several intresting possibilities to explore: for
instance, we can build F# Async-like computations in ATS without much
runtime overhead.

Does anybody have a working patsopt to compile this code and run it? All I
know is that it type-checks.

The idea is okay in principle. However, there are several issues that
need to be addressed. Basically, the way in which templates are expanded in
ATS2 is not precisely like what you might have thought.

Thanks!

The takeaway, IIUC, is that for templates to work in this case, the user
has to specify template parameters (in angular braces) in all template
function applications.

I would just use the standard style.
‘gcc -O3’ should eliminate actual closure formation.
You still need -DATS_MEMALLOC_LIBC because option-values
are heap-allocated.

(* ****** ****** )
//
#include
“share/atspre_define.hats”
#include
“share/atspre_staload.hats”
//
(
****** ****** *)

abst@ype M (t@ype) = ptr

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

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

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

local

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

in (* in-of-local *)

implement
{a}(tmp)
ret (x) = Some x

implement
{a,b}
bind (x, f) = let
//
val () = println! (“bind: x = …”)
//
in
//
case+ x of
| Some x => f (x) | None () => None ()
//
end // end of [bind]

fun{a:t@ype}
runM (x : M(a)): a =
case+ x of
| Some x => x
| None () => exit_errmsg (1, “runM failed!”)

end // end of [local]

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

infix >>=

(* ****** ****** *)
//
extern
fun
mytest
(x: int) : M(int) = “mytest”
//
implement
mytest (x) = let
//
macdef >>=(x, f) = bind<int,int>(,(x), ,(f))
//
in
//
ret(10)

= (lam(y) =>
ret(100)
= (lam(z) =>
ret (x + y + z)
)
)
//
end // end of [test]

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

implement
main0 (argc, argv) = let
val comp = mytest (argc)
// specify the type explicitly
val res = runM (comp)
in
println!("result = ", res);
end // end of [main]

(* ****** ****** *)On Wednesday, December 31, 2014 10:57:00 PM UTC-5, Artyom Shalkhakov wrote:

On Thursday, January 1, 2015 6:44:51 AM UTC+6, gmhwxi wrote:

The idea is okay in principle. However, there are several issues that
need to be addressed. Basically, the way in which templates are expanded
in
ATS2 is not precisely like what you might have thought.

Thanks!

The takeaway, IIUC, is that for templates to work in this case, the user
has to specify template parameters (in angular braces) in all template
function applications.

Here is a working version:

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

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

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

// the interface

abst@ype M (t@ype) = ptr

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

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

symintr >>=
postfix >>=
overload >>= with bind

// we replace the second argument of bind with a function template
// which should allow the ATS compiler to inline aggressively
extern
fun{a,b:t@ype}
bind$cont (x: a): M(b)

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

extern
fun{a,b:t@ype}
bind1 : M(a) → M(b)
extern
fun{a,b:t@ype}
bind2 : M(a) → M(b)

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

// one possible implementation

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

// an explicit failure function (cf. MonadFail)
fun Mfail {a:t@ype} (): M(a) = None ()

implement
{a}(tmp)
ret (x) = Some x

implement
{a,b}
bind (x) = let
//
val () = println! (“bind: x = …”)
//
in
//
case+ x of
| Some x => bind$cont<a,b>(x) | None () => None ()
//
end // end of [bind]

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

implement
{a,b}
bind1 (x) = let
//
val () = println! (“bind1: x = …”)
//
in
//
case+ x of
| Some x => bind$cont<a,b>(x) | None () => None ()
//
end // end of [bind1]

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

implement
{a,b}
bind2 (x) = let
//
val () = println! (“bind2: x = …”)
//
in
//
case+ x of
| Some x => bind$cont<a,b>(x) | None () => None ()
//
end // end of [bind2]

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

// a Maybe monad can be run
fun{a:t@ype} runM (x : M(a)): a =
case+ x of
| Some x => x
| None () => exit_errmsg (1, “runM failed!”)

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

// usage example
// this computation doesn’t know anything about the internals
// of the implementation of the underlying monad, I think
fun test (x : int): M int =
ret 5 >>= where {implement bind$cont<int,int> (y) =
ret 4 >>= where {implement bind$cont<int,int> (z) =
ret (x + y + z)}}
)
(

fun test (x : int): M int =
bind<int,int>(ret(5)) where {implement bind$cont<int,int> (y) =
bind<int,int>(ret(4)) where {implement bind$cont<int,int> (z) =
ret (x + y + z)}}
)
(

fun test (x : int): M int = ret(x)
)
(

fun
test (x : int): M int =
bind<int,int>(ret(10)) where
{
implement bind$cont<int,int> (y) = ret (x + y)
}
*)

fun
test
(
x : int
) : M int = let
//
implement
bind$cont<int,int> (y) = let
//
val () = println! ("bind$cont(1): y = ", y)
//
implement
bind$cont<int,int> (z) = let
//
val () = println! (“bind$cont: 2”) in ret (x + y + z)
//
end // end of [bind$cont]
//
in
bind1<int,int> (ret(10))
end // end of [bind$cont]
//
in
bind2<int,int> (ret(100))
end // end of [test]

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

implement
main0 (argc, argv) = let
val comp = test (argc)
// specify the type explicitly
val res = runM (comp)
in
println!("result = ", res);
end // end of [main]

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

On Wednesday, December 31, 2014 10:40:46 AM UTC-5, Artyom Shalkhakov wrote:

Here’s something a came up with:

Encoding monads in ATS2 with function templates · GitHub

This shows a Maybe monad from Haskell in ATS/Postiats. The idea is that
no higher-order functions are involved (and no closures too). If it works,
then it means we have several intresting possibilities to explore: for
instance, we can build F# Async-like computations in ATS without much
runtime overhead.

Does anybody have a working patsopt to compile this code and run it? All
I know is that it type-checks.

The idea is okay in principle. However, there are several issues that
need to be addressed. Basically, the way in which templates are expanded in
ATS2 is not precisely like what you might have thought.

Here is a working version:

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

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

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

// the interface

abst@ype M (t@ype) = ptr

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

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

symintr >>=
postfix >>=
overload >>= with bind

// we replace the second argument of bind with a function template
// which should allow the ATS compiler to inline aggressively
extern
fun{a,b:t@ype}
bind$cont (x: a): M(b)

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

extern
fun{a,b:t@ype}
bind1 : M(a) → M(b)
extern
fun{a,b:t@ype}
bind2 : M(a) → M(b)

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

// one possible implementation

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

// an explicit failure function (cf. MonadFail)
fun Mfail {a:t@ype} (): M(a) = None ()

implement
{a}(tmp)
ret (x) = Some x

implement
{a,b}
bind (x) = let
//
val () = println! (“bind: x = …”)
//
in
//
case+ x of
| Some x => bind$cont<a,b>(x) | None () => None ()
//
end // end of [bind]

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

implement
{a,b}
bind1 (x) = let
//
val () = println! (“bind1: x = …”)
//
in
//
case+ x of
| Some x => bind$cont<a,b>(x) | None () => None ()
//
end // end of [bind1]

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

implement
{a,b}
bind2 (x) = let
//
val () = println! (“bind2: x = …”)
//
in
//
case+ x of
| Some x => bind$cont<a,b>(x) | None () => None ()
//
end // end of [bind2]

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

// a Maybe monad can be run
fun{a:t@ype} runM (x : M(a)): a =
case+ x of
| Some x => x
| None () => exit_errmsg (1, “runM failed!”)

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

// usage example
// this computation doesn’t know anything about the internals
// of the implementation of the underlying monad, I think
fun test (x : int): M int =
ret 5 >>= where {implement bind$cont<int,int> (y) =
ret 4 >>= where {implement bind$cont<int,int> (z) =
ret (x + y + z)}}
)
(

fun test (x : int): M int =
bind<int,int>(ret(5)) where {implement bind$cont<int,int> (y) =
bind<int,int>(ret(4)) where {implement bind$cont<int,int> (z) =
ret (x + y + z)}}
)
(

fun test (x : int): M int = ret(x)
)
(

fun
test (x : int): M int =
bind<int,int>(ret(10)) where
{
implement bind$cont<int,int> (y) = ret (x + y)
}
*)

fun
test
(
x : int
) : M int = let
//
implement
bind$cont<int,int> (y) = let
//
val () = println! ("bind$cont(1): y = ", y)
//
implement
bind$cont<int,int> (z) = let
//
val () = println! (“bind$cont: 2”) in ret (x + y + z)
//
end // end of [bind$cont]
//
in
bind1<int,int> (ret(10))
end // end of [bind$cont]
//
in
bind2<int,int> (ret(100))
end // end of [test]

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

implement
main0 (argc, argv) = let
val comp = test (argc)
// specify the type explicitly
val res = runM (comp)
in
println!("result = ", res);
end // end of [main]

(* ****** ****** *)On Wednesday, December 31, 2014 10:40:46 AM UTC-5, Artyom Shalkhakov wrote:

Here’s something a came up with:

Encoding monads in ATS2 with function templates · GitHub

This shows a Maybe monad from Haskell in ATS/Postiats. The idea is that no
higher-order functions are involved (and no closures too). If it works,
then it means we have several intresting possibilities to explore: for
instance, we can build F# Async-like computations in ATS without much
runtime overhead.

Does anybody have a working patsopt to compile this code and run it? All I
know is that it type-checks.

I added some code to show that (original) Haskell-like syntax for using
monads can be simulated
in ATS (to a large degree):

When you write

ret(x) >>= (lam (y) => …) // >>= is infix for bind

‘gcc-O3’ should be able to optimize away the need to actually form a
closure to pass to >>= as long as
the definition of >>= is available.On Wednesday, December 31, 2014 11:37:08 PM UTC-5, gmhwxi wrote:

I would just use the standard style.
‘gcc -O3’ should eliminate actual closure formation.
You still need -DATS_MEMALLOC_LIBC because option-values
are heap-allocated.

(* ****** ****** )
//
#include
“share/atspre_define.hats”
#include
“share/atspre_staload.hats”
//
(
****** ****** *)

abst@ype M (t@ype) = ptr

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

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

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

local

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

in (* in-of-local *)

implement
{a}(tmp)
ret (x) = Some x

implement
{a,b}
bind (x, f) = let
//
val () = println! (“bind: x = …”)
//
in
//
case+ x of
| Some x => f (x) | None () => None ()
//
end // end of [bind]

fun{a:t@ype}
runM (x : M(a)): a =
case+ x of
| Some x => x
| None () => exit_errmsg (1, “runM failed!”)

end // end of [local]

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

infix >>=

(* ****** ****** *)
//
extern
fun
mytest
(x: int) : M(int) = “mytest”
//
implement
mytest (x) = let
//
macdef >>=(x, f) = bind<int,int>(,(x), ,(f))
//
in
//
ret(10)

= (lam(y) =>
ret(100)
= (lam(z) =>
ret (x + y + z)
)
)
//
end // end of [test]

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

implement
main0 (argc, argv) = let
val comp = mytest (argc)
// specify the type explicitly
val res = runM (comp)
in
println!("result = ", res);
end // end of [main]

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

On Wednesday, December 31, 2014 10:57:00 PM UTC-5, Artyom Shalkhakov wrote:

On Thursday, January 1, 2015 6:44:51 AM UTC+6, gmhwxi wrote:

The idea is okay in principle. However, there are several issues that
need to be addressed. Basically, the way in which templates are expanded in
ATS2 is not precisely like what you might have thought.

Thanks!

The takeaway, IIUC, is that for templates to work in this case, the user
has to specify template parameters (in angular braces) in all template
function applications.

Here is a working version:

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

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

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

// the interface

abst@ype M (t@ype) = ptr

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

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

symintr >>=
postfix >>=
overload >>= with bind

// we replace the second argument of bind with a function template
// which should allow the ATS compiler to inline aggressively
extern
fun{a,b:t@ype}
bind$cont (x: a): M(b)

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

extern
fun{a,b:t@ype}
bind1 : M(a) → M(b)
extern
fun{a,b:t@ype}
bind2 : M(a) → M(b)

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

// one possible implementation

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

// an explicit failure function (cf. MonadFail)
fun Mfail {a:t@ype} (): M(a) = None ()

implement
{a}(tmp)
ret (x) = Some x

implement
{a,b}
bind (x) = let
//
val () = println! (“bind: x = …”)
//
in
//
case+ x of
| Some x => bind$cont<a,b>(x) | None () => None ()
//
end // end of [bind]

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

implement
{a,b}
bind1 (x) = let
//
val () = println! (“bind1: x = …”)
//
in
//
case+ x of
| Some x => bind$cont<a,b>(