Fuctorial map

Aistis_Raulinaitis · September 22, 2015, 4:12am

Implementing F-Algebras in ATS, wondering what I’m doing wrong or where
should I be looking? So far I have:

datatype Algebra (f:t@ype -> t@ype,a:t@ype) = Algebra of (f a)

datatype Fix (f:t@ype -> t@ype) = Iso of @{ invIso = f (Fix f) }

fun cata {f:t@ype -> t@ype}{a:t@ype} (alg:Algebra (f,a)): (Fix f -> a) =
lam (f) => alg (map (cata alg) (f.invIso))

The last line does compile, says that map is out of scope. Where would I
get it? Mind you, f is a Functor.

gmhwxi · September 23, 2015, 6:23pm

If you compile to JavaScript, using t@ype is fine.
However, if you do not use closures, you will encounter
some compilation errors even if the code passes typechecking.On Wednesday, September 23, 2015 at 1:59:45 PM UTC-4, Aistis Raulinaitis wrote:

Also:

extern fun fexpr_eval : Algebra (Fexpr, int)

Sorry for the triple post!

So in all:

sortdef ftype = t@ype → t@ype

typedef Functor (f:ftype) = {a,b:t@ype} (a → b) → f a → f b

typedef Algebra (f:ftype, a:t@ype) = f a → a

datatype Fix (f:ftype) = Fx of f (Fix f)

extern fun fix_unfold {f:ftype} : Fix f → f (Fix f)
implement fix_unfold (Fx f) = f

extern fun cata : {f:ftype} {a:t@ype} Functor f → Algebra (f, a) → (Fix
f → a)
implement cata map = lam alg => lam f => alg (map (cata map alg) (fix_unfold
f))

datatype Fexpr (a:t@ype)
= Int of int
| Add of (a, a)
| Mul of (a, a)

typedef Expr = Fix Fexpr

extern val fexpr_map : Functor Fexpr
implement fexpr_map f = lam e0 => ( case+ e0 of
| Int i => Int i
| Add (a, b) => Add (f a, f b)
| Mul (a, b) => Mul (f a, f b))

extern fun fexpr_eval : Algebra (Fexpr, int)
implement fexpr_eval e0 = ( case+ e0 of
| Int i => i
| Add (a, b) => a + b
| Mul (a, b) => a * b)

val I1 = Fx (Int 1) : Expr
val I2 = Fx (Int 2) : Expr
val I3 = Fx (Int 3) : Expr
val Mul_2_3 = Fx (Mul (I2, I3)) : Expr
val Add_1_Mul_2_3 = Fx (Add (I1, Mul_2_3)) : Expr

val Ans = cata fexpr_map fexpr_eval Add_1_Mul_2_3

val () = println! ("eval(1+2*3) = ", Ans)

implement main0 () = ()

On Monday, September 21, 2015 at 9:12:19 PM UTC-7, Aistis Raulinaitis wrote:

Implementing F-Algebras in ATS, wondering what I’m doing wrong or where
should I be looking? So far I have:

datatype Algebra (f:t@ype → t@ype,a:t@ype) = Algebra of (f a)

datatype Fix (f:t@ype → t@ype) = Iso of @{ invIso = f (Fix f) }

fun cata {f:t@ype → t@ype}{a:t@ype} (alg:Algebra (f,a)): (Fix f → a) =
lam (f) => alg (map (cata alg) (f.invIso))

The last line does compile, says that map is out of scope. Where would I
get it? Mind you, f is a Functor.

Aistis_Raulinaitis · September 23, 2015, 5:35pm

Actually it’s a lot simpler, no need for Box, or cloref1, as well as you
can implement it over t@ype. At least it typechecks…

sortdef ftype = t@ype → t@ype

typedef Functor (f:ftype) = {a,b:t@ype} (a → b) → f a → f b

typedef Algebra (f:ftype, a:t@ype) = f a → a

datatype Fix (f:ftype) = Fx of f (Fix f)

extern fun fix_unfold {f:ftype} : Fix f → f (Fix f)
implement fix_unfold f = let val+ Fx f = f in f end

extern fun cata : {f:ftype}{a:t@ype} Functor f → Algebra (f, a) → (Fix f
→ a)
implement cata map = lam alg => lam f => alg (map (cata map alg) (fix_unfold
f))

datatype Fexpr (a:t@ype)
= Int of int
| Add of (a, a)
| Mul of (a, a)

typedef Expr = Fix Fexpr

extern val fexpr_map : Functor Fexpr
implement fexpr_map f = lam e0 => ( case+ e0 of
| Int i => Int i
| Add (a, b) => Add (f a, f b)
| Mul (a, b) => Mul (f a, f b))

extern fun fexpr_eval : Fexpr int → int
implement fexpr_eval e0 = ( case+ e0 of
| Int i => i
| Add (a, b) => a + b
| Mul (a, b) => a * b)

val I1 = Fx (Int 1): Expr
val I2 = Fx (Int 2): Expr
val I3 = Fx (Int 3): Expr
val Mul_2_3 = Fx (Mul (I2, I3)): Expr
val Add_1_Mul_2_3 = Fx (Add (I1, Mul_2_3)): Expr

val Ans = cata fexpr_map fexpr_eval Add_1_Mul_2_3

val () = println! ("eval(1+2*3) = ", Ans)

implement main0 () = ()On Tuesday, September 22, 2015 at 10:41:05 AM UTC-7, gmhwxi wrote:

This one works on-line:

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats/master/doc/EXAMPLE/ATSLF/F-algebra_js.dats

On Tuesday, September 22, 2015 at 1:01:51 PM UTC-4, Aistis Raulinaitis wrote:

Beautiful! Thanks!

On Tue, Sep 22, 2015 at 7:22 AM, gmhwxi gmh...@gmail.com wrote:

For a bit fun, I get the F-algebra code running:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATSLF/F-algebra.dats

Well, it must be a bit crazy to program like this

On Tuesday, September 22, 2015 at 9:01:38 AM UTC-4, gmhwxi wrote:

Here is something that typechecks:

(* ****** ****** )
//
infixr (->) ->>
//
typedef
->> (a:type, b:type) = a - b
//
( ****** ****** *)

sortdef
ftype = type → type
typedef
Algebra (f:ftype, a:type) = f(a) ->> a

(* ****** ****** )
//
extern
fun Map{f:ftype}{a,b:type} (a ->> b): f a ->> f b
//
( ****** ****** *)

(*
datatype
Fix (f:type → type) = Iso of @{ invIso = f (Fix f) }
*)

abstype
Fix(f:type → type)
extern fun Fix_unfold{f:ftype} : Fix(f) → f (Fix(f))

(* ****** ****** )
//
fun
cata{f:ftype}{a:type}
(alg: Algebra (f,a)): (Fix f ->> a) =
lam (f: Fix(f)) => alg(Map(cata(alg))(Fix_unfold(f)))
//
( ****** ****** *)

On Tuesday, September 22, 2015 at 12:12:19 AM UTC-4, Aistis Raulinaitis wrote:

Implementing F-Algebras in ATS, wondering what I’m doing wrong or
where should I be looking? So far I have:

datatype Algebra (f:t@ype → t@ype,a:t@ype) = Algebra of (f a)

datatype Fix (f:t@ype → t@ype) = Iso of @{ invIso = f (Fix f) }

fun cata {f:t@ype → t@ype}{a:t@ype} (alg:Algebra (f,a)): (Fix f → a)
= lam (f) => alg (map (cata alg) (f.invIso))

The last line does compile, says that map is out of scope. Where would
I get it? Mind you, f is a Functor.

–
You received this message because you are subscribed to a topic in the
Google Groups “ats-lang-users” group.
To unsubscribe from this topic, visit
https://groups.google.com/d/topic/ats-lang-users/tfEnAR2vIOA/unsubscribe
.
To unsubscribe from this group and all its topics, send an email to
ats-lang...@googlegroups.com.
To post to this group, send email to ats-l...@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/28a6f4f6-a0ee-4065-a5cb-b3bfa34a36c3%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/28a6f4f6-a0ee-4065-a5cb-b3bfa34a36c3%40googlegroups.com?utm_medium=email&utm_source=footer
.

gmhwxi · September 26, 2015, 3:13am

This is due to a new feature ($d2ctype) being used in this example.

I have just uploaded a modified version that does not use this new feature.On Fri, Sep 25, 2015 at 11:01 PM, Aistis Raulinaitis shega...@gmail.com wrote:

The typechecker complains with:

patsopt -tc -d
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
639(line=50, offs=7) – 647(line=50, offs=15): error(parsing): the
syntactic entity [s0taq] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
639(line=50, offs=7) – 647(line=50, offs=15): error(parsing): the
syntactic entity [si0de] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
639(line=50, offs=7) – 647(line=50, offs=15): error(parsing): the
syntactic entity [s0exp] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
637(line=50, offs=5) – 638(line=50, offs=6): error(parsing): the keyword
[=] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
629(line=49, offs=1) – 632(line=49, offs=4): error(parsing): the keyword
‘}’ is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
610(line=46, offs=17) – 613(line=46, offs=20): error(parsing): the
syntactic entity [d0exp] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
573(line=44, offs=1) – 582(line=44, offs=10): error(parsing): the token is
discarded.
exit(ATS): uncaught exception:
_2home_2hwxi_2research_2Postiats_2git_2src_2pats_error_2esats__FatalErrorExn(1025)

Compilation exited abnormally with code 1 at Fri Sep 25 19:57:55

On Thursday, September 24, 2015 at 7:30:29 PM UTC-7, gmhwxi wrote:

I studied this cata-example a bit more.

As it stands now, this implementation is terribly slow.

I would like to suggest the following style of template-based
implementation of cata:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/TESTATS/catamorph.dats

I think it is quite involved to get the Haskell code (implementing
F-algebra) to run efficiently.
Cata(map) is clearly defined recursively and compiling it into efficient
code likely needs to have
deforestation optimization turned on.

The template-based implementation of cata in ATS does not create any
trees, and there is no ‘Fix’
clutter, either. All that is really needed for compiling the
implementation into efficient code is to inline
function calls aggressively.

On Wednesday, September 23, 2015 at 1:42:36 PM UTC-4, Aistis Raulinaitis wrote:

The nice thing about F-algebras is that you can define fexpr_eval
non-recursively. It’s quite fast, a lot of performant libs in Haskell are
written in terms of F-algebras. It’s especially good for languages that
don’t handle recursion well, and a succinct way of defining ASTs.

Also, you can simplify fix_unfold:

extern fun fix_unfold {f:ftype} : Fix f → f (Fix f)
implement fix_unfold (Fx f) = f

On Tuesday, September 22, 2015 at 10:41:05 AM UTC-7, gmhwxi wrote:

This one works on-line:

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats/master/doc/EXAMPLE/ATSLF/F-algebra_js.dats

On Tuesday, September 22, 2015 at 1:01:51 PM UTC-4, Aistis Raulinaitis wrote:

Beautiful! Thanks!

On Tue, Sep 22, 2015 at 7:22 AM, gmhwxi gmh...@gmail.com wrote:

For a bit fun, I get the F-algebra code running:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATSLF/F-algebra.dats

Well, it must be a bit crazy to program like this

On Tuesday, September 22, 2015 at 9:01:38 AM UTC-4, gmhwxi wrote:

Here is something that typechecks:

(* ****** ****** )
//
infixr (->) ->>
//
typedef
->> (a:type, b:type) = a - b
//
( ****** ****** *)

sortdef
ftype = type → type
typedef
Algebra (f:ftype, a:type) = f(a) ->> a

(* ****** ****** )
//
extern
fun Map{f:ftype}{a,b:type} (a ->> b): f a ->> f b
//
( ****** ****** *)

(*
datatype
Fix (f:type → type) = Iso of @{ invIso = f (Fix f) }
*)

abstype
Fix(f:type → type)
extern fun Fix_unfold{f:ftype} : Fix(f) → f (Fix(f))

(* ****** ****** )
//
fun
cata{f:ftype}{a:type}
(alg: Algebra (f,a)): (Fix f ->> a) =
lam (f: Fix(f)) => alg(Map(cata(alg))(Fix_unfold(f)))
//
( ****** ****** *)

On Tuesday, September 22, 2015 at 12:12:19 AM UTC-4, Aistis Raulinaitis wrote:

Implementing F-Algebras in ATS, wondering what I’m doing wrong or
where should I be looking? So far I have:

datatype Algebra (f:t@ype → t@ype,a:t@ype) = Algebra of (f a)

datatype Fix (f:t@ype → t@ype) = Iso of @{ invIso = f (Fix f) }

fun cata {f:t@ype → t@ype}{a:t@ype} (alg:Algebra (f,a)): (Fix f →
a) = lam (f) => alg (map (cata alg) (f.invIso))

The last line does compile, says that map is out of scope. Where
would I get it? Mind you, f is a Functor.

–
You received this message because you are subscribed to a topic in
the Google Groups “ats-lang-users” group.
To unsubscribe from this topic, visit
https://groups.google.com/d/topic/ats-lang-users/tfEnAR2vIOA/unsubscribe
.
To unsubscribe from this group and all its topics, send an email to
ats-lang...@googlegroups.com.
To post to this group, send email to ats-l...@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/28a6f4f6-a0ee-4065-a5cb-b3bfa34a36c3%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/28a6f4f6-a0ee-4065-a5cb-b3bfa34a36c3%40googlegroups.com?utm_medium=email&utm_source=footer
.

–
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/a59e0bc4-6148-4e0f-bab8-b2a7b2104bc5%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/a59e0bc4-6148-4e0f-bab8-b2a7b2104bc5%40googlegroups.com?utm_medium=email&utm_source=footer
.

Aistis_Raulinaitis · September 26, 2015, 3:44am

Interesting, what does $d2ctype do?On Fri, Sep 25, 2015 at 8:13 PM, Hongwei Xi gmh...@gmail.com wrote:

This is due to a new feature ($d2ctype) being used in this example.

I have just uploaded a modified version that does not use this new feature.

On Fri, Sep 25, 2015 at 11:01 PM, Aistis Raulinaitis < shega...@gmail.com> wrote:

The typechecker complains with:

patsopt -tc -d
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
639(line=50, offs=7) – 647(line=50, offs=15): error(parsing): the
syntactic entity [s0taq] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
639(line=50, offs=7) – 647(line=50, offs=15): error(parsing): the
syntactic entity [si0de] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
639(line=50, offs=7) – 647(line=50, offs=15): error(parsing): the
syntactic entity [s0exp] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
637(line=50, offs=5) – 638(line=50, offs=6): error(parsing): the keyword
[=] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
629(line=49, offs=1) – 632(line=49, offs=4): error(parsing): the keyword
‘}’ is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
610(line=46, offs=17) – 613(line=46, offs=20): error(parsing): the
syntactic entity [d0exp] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
573(line=44, offs=1) – 582(line=44, offs=10): error(parsing): the token is
discarded.
exit(ATS): uncaught exception:
_2home_2hwxi_2research_2Postiats_2git_2src_2pats_error_2esats__FatalErrorExn(1025)

Compilation exited abnormally with code 1 at Fri Sep 25 19:57:55

On Thursday, September 24, 2015 at 7:30:29 PM UTC-7, gmhwxi wrote:

I studied this cata-example a bit more.

As it stands now, this implementation is terribly slow.

I would like to suggest the following style of template-based
implementation of cata:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/TESTATS/catamorph.dats

I think it is quite involved to get the Haskell code (implementing
F-algebra) to run efficiently.
Cata(map) is clearly defined recursively and compiling it into efficient
code likely needs to have
deforestation optimization turned on.

The template-based implementation of cata in ATS does not create any
trees, and there is no ‘Fix’
clutter, either. All that is really needed for compiling the
implementation into efficient code is to inline
function calls aggressively.

On Wednesday, September 23, 2015 at 1:42:36 PM UTC-4, Aistis Raulinaitis wrote:

The nice thing about F-algebras is that you can define fexpr_eval
non-recursively. It’s quite fast, a lot of performant libs in Haskell are
written in terms of F-algebras. It’s especially good for languages that
don’t handle recursion well, and a succinct way of defining ASTs.

Also, you can simplify fix_unfold:

extern fun fix_unfold {f:ftype} : Fix f → f (Fix f)
implement fix_unfold (Fx f) = f

On Tuesday, September 22, 2015 at 10:41:05 AM UTC-7, gmhwxi wrote:

This one works on-line:

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats/master/doc/EXAMPLE/ATSLF/F-algebra_js.dats

On Tuesday, September 22, 2015 at 1:01:51 PM UTC-4, Aistis Raulinaitis wrote:

Beautiful! Thanks!

On Tue, Sep 22, 2015 at 7:22 AM, gmhwxi gmh...@gmail.com wrote:

For a bit fun, I get the F-algebra code running:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATSLF/F-algebra.dats

Well, it must be a bit crazy to program like this

On Tuesday, September 22, 2015 at 9:01:38 AM UTC-4, gmhwxi wrote:

Here is something that typechecks:

(* ****** ****** )
//
infixr (->) ->>
//
typedef
->> (a:type, b:type) = a - b
//
( ****** ****** *)

sortdef
ftype = type → type
typedef
Algebra (f:ftype, a:type) = f(a) ->> a

(* ****** ****** )
//
extern
fun Map{f:ftype}{a,b:type} (a ->> b): f a ->> f b
//
( ****** ****** *)

(*
datatype
Fix (f:type → type) = Iso of @{ invIso = f (Fix f) }
*)

abstype
Fix(f:type → type)
extern fun Fix_unfold{f:ftype} : Fix(f) → f (Fix(f))

(* ****** ****** )
//
fun
cata{f:ftype}{a:type}
(alg: Algebra (f,a)): (Fix f ->> a) =
lam (f: Fix(f)) => alg(Map(cata(alg))(Fix_unfold(f)))
//
( ****** ****** *)

On Tuesday, September 22, 2015 at 12:12:19 AM UTC-4, Aistis Raulinaitis wrote:

Implementing F-Algebras in ATS, wondering what I’m doing wrong or
where should I be looking? So far I have:

datatype Algebra (f:t@ype → t@ype,a:t@ype) = Algebra of (f a)

datatype Fix (f:t@ype → t@ype) = Iso of @{ invIso = f (Fix f) }

fun cata {f:t@ype → t@ype}{a:t@ype} (alg:Algebra (f,a)): (Fix f
→ a) = lam (f) => alg (map (cata alg) (f.invIso))

The last line does compile, says that map is out of scope. Where
would I get it? Mind you, f is a Functor.

–
You received this message because you are subscribed to a topic in
the Google Groups “ats-lang-users” group.
To unsubscribe from this topic, visit
https://groups.google.com/d/topic/ats-lang-users/tfEnAR2vIOA/unsubscribe
.
To unsubscribe from this group and all its topics, send an email to
ats-lang...@googlegroups.com.
To post to this group, send email to ats-l...@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/28a6f4f6-a0ee-4065-a5cb-b3bfa34a36c3%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/28a6f4f6-a0ee-4065-a5cb-b3bfa34a36c3%40googlegroups.com?utm_medium=email&utm_source=footer
.

–
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/a59e0bc4-6148-4e0f-bab8-b2a7b2104bc5%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/a59e0bc4-6148-4e0f-bab8-b2a7b2104bc5%40googlegroups.com?utm_medium=email&utm_source=footer
.

–
You received this message because you are subscribed to a topic in the
Google Groups “ats-lang-users” group.
To unsubscribe from this topic, visit
https://groups.google.com/d/topic/ats-lang-users/tfEnAR2vIOA/unsubscribe.
To unsubscribe from this group and all its topics, 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/CAPPSPLqU6hSBn9mmjRpoy%3DXA1rZq8YMvzWYkMnfB7uuSu73AAA%40mail.gmail.com
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLqU6hSBn9mmjRpoy%3DXA1rZq8YMvzWYkMnfB7uuSu73AAA%40mail.gmail.com?utm_medium=email&utm_source=footer
.

gmhwxi · September 22, 2015, 11:11am

At one point implemented Yoneda lemma and co-Yoneda lemma:

I remember that I had to use type instead of t@ype.On Tuesday, September 22, 2015 at 12:44:31 AM UTC-4, Aistis Raulinaitis wrote:

Also yes, Algebra should be defined as:

typedef Algebra (f:t@ype → t@ype,a:t@ype) = f a → a

I don’t know what I copied…

On Monday, September 21, 2015 at 9:12:19 PM UTC-7, Aistis Raulinaitis wrote:

Implementing F-Algebras in ATS, wondering what I’m doing wrong or where
should I be looking? So far I have:

datatype Algebra (f:t@ype → t@ype,a:t@ype) = Algebra of (f a)

datatype Fix (f:t@ype → t@ype) = Iso of @{ invIso = f (Fix f) }

fun cata {f:t@ype → t@ype}{a:t@ype} (alg:Algebra (f,a)): (Fix f → a) =
lam (f) => alg (map (cata alg) (f.invIso))

The last line does compile, says that map is out of scope. Where would I
get it? Mind you, f is a Functor.

Aistis_Raulinaitis · September 22, 2015, 5:01pm

Beautiful! Thanks!On Tue, Sep 22, 2015 at 7:22 AM, gmhwxi gmh...@gmail.com wrote:

For a bit fun, I get the F-algebra code running:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATSLF/F-algebra.dats

Well, it must be a bit crazy to program like this

On Tuesday, September 22, 2015 at 9:01:38 AM UTC-4, gmhwxi wrote:

Here is something that typechecks:

(* ****** ****** )
//
infixr (->) ->>
//
typedef
->> (a:type, b:type) = a - b
//
( ****** ****** *)

sortdef
ftype = type → type
typedef
Algebra (f:ftype, a:type) = f(a) ->> a

(* ****** ****** )
//
extern
fun Map{f:ftype}{a,b:type} (a ->> b): f a ->> f b
//
( ****** ****** *)

(*
datatype
Fix (f:type → type) = Iso of @{ invIso = f (Fix f) }
*)

abstype
Fix(f:type → type)
extern fun Fix_unfold{f:ftype} : Fix(f) → f (Fix(f))

(* ****** ****** )
//
fun
cata{f:ftype}{a:type}
(alg: Algebra (f,a)): (Fix f ->> a) =
lam (f: Fix(f)) => alg(Map(cata(alg))(Fix_unfold(f)))
//
( ****** ****** *)

On Tuesday, September 22, 2015 at 12:12:19 AM UTC-4, Aistis Raulinaitis wrote:

Implementing F-Algebras in ATS, wondering what I’m doing wrong or where
should I be looking? So far I have:

datatype Algebra (f:t@ype → t@ype,a:t@ype) = Algebra of (f a)

datatype Fix (f:t@ype → t@ype) = Iso of @{ invIso = f (Fix f) }

fun cata {f:t@ype → t@ype}{a:t@ype} (alg:Algebra (f,a)): (Fix f → a) =
lam (f) => alg (map (cata alg) (f.invIso))

The last line does compile, says that map is out of scope. Where would I
get it? Mind you, f is a Functor.

–
You received this message because you are subscribed to a topic in the
Google Groups “ats-lang-users” group.
To unsubscribe from this topic, visit
https://groups.google.com/d/topic/ats-lang-users/tfEnAR2vIOA/unsubscribe.
To unsubscribe from this group and all its topics, 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/28a6f4f6-a0ee-4065-a5cb-b3bfa34a36c3%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/28a6f4f6-a0ee-4065-a5cb-b3bfa34a36c3%40googlegroups.com?utm_medium=email&utm_source=footer
.

gmhwxi · September 22, 2015, 5:41pm

This one works on-line:

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats/master/doc/EXAMPLE/ATSLF/F-algebra_js.datsOn Tuesday, September 22, 2015 at 1:01:51 PM UTC-4, Aistis Raulinaitis wrote:

Beautiful! Thanks!

On Tue, Sep 22, 2015 at 7:22 AM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

For a bit fun, I get the F-algebra code running:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATSLF/F-algebra.dats

Well, it must be a bit crazy to program like this

On Tuesday, September 22, 2015 at 9:01:38 AM UTC-4, gmhwxi wrote:

Here is something that typechecks:

(* ****** ****** )
//
infixr (->) ->>
//
typedef
->> (a:type, b:type) = a - b
//
( ****** ****** *)

sortdef
ftype = type → type
typedef
Algebra (f:ftype, a:type) = f(a) ->> a

(* ****** ****** )
//
extern
fun Map{f:ftype}{a,b:type} (a ->> b): f a ->> f b
//
( ****** ****** *)

(*
datatype
Fix (f:type → type) = Iso of @{ invIso = f (Fix f) }
*)

abstype
Fix(f:type → type)
extern fun Fix_unfold{f:ftype} : Fix(f) → f (Fix(f))

(* ****** ****** )
//
fun
cata{f:ftype}{a:type}
(alg: Algebra (f,a)): (Fix f ->> a) =
lam (f: Fix(f)) => alg(Map(cata(alg))(Fix_unfold(f)))
//
( ****** ****** *)

On Tuesday, September 22, 2015 at 12:12:19 AM UTC-4, Aistis Raulinaitis wrote:

Implementing F-Algebras in ATS, wondering what I’m doing wrong or where
should I be looking? So far I have:

datatype Algebra (f:t@ype → t@ype,a:t@ype) = Algebra of (f a)

datatype Fix (f:t@ype → t@ype) = Iso of @{ invIso = f (Fix f) }

fun cata {f:t@ype → t@ype}{a:t@ype} (alg:Algebra (f,a)): (Fix f → a)
= lam (f) => alg (map (cata alg) (f.invIso))

The last line does compile, says that map is out of scope. Where would
I get it? Mind you, f is a Functor.

–
You received this message because you are subscribed to a topic in the
Google Groups “ats-lang-users” group.
To unsubscribe from this topic, visit
https://groups.google.com/d/topic/ats-lang-users/tfEnAR2vIOA/unsubscribe.
To unsubscribe from this group and all its topics, send an email to
ats-lang...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
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/28a6f4f6-a0ee-4065-a5cb-b3bfa34a36c3%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/28a6f4f6-a0ee-4065-a5cb-b3bfa34a36c3%40googlegroups.com?utm_medium=email&utm_source=footer
.

Aistis_Raulinaitis · September 22, 2015, 4:44am

Also yes, Algebra should be defined as:

typedef Algebra (f:t@ype → t@ype,a:t@ype) = f a → a

I don’t know what I copied…On Monday, September 21, 2015 at 9:12:19 PM UTC-7, Aistis Raulinaitis wrote:

Implementing F-Algebras in ATS, wondering what I’m doing wrong or where
should I be looking? So far I have:

datatype Algebra (f:t@ype → t@ype,a:t@ype) = Algebra of (f a)

datatype Fix (f:t@ype → t@ype) = Iso of @{ invIso = f (Fix f) }

fun cata {f:t@ype → t@ype}{a:t@ype} (alg:Algebra (f,a)): (Fix f → a) =
lam (f) => alg (map (cata alg) (f.invIso))

The last line does compile, says that map is out of scope. Where would I
get it? Mind you, f is a Functor.

Aistis_Raulinaitis · September 23, 2015, 5:42pm

The nice thing about F-algebras is that you can define fexpr_eval
non-recursively. It’s quite fast, a lot of performant libs in Haskell are
written in terms of F-algebras. It’s especially good for languages that
don’t handle recursion well, and a succinct way of defining ASTs.

Also, you can simplify fix_unfold:

extern fun fix_unfold {f:ftype} : Fix f → f (Fix f)
implement fix_unfold (Fx f) = fOn Tuesday, September 22, 2015 at 10:41:05 AM UTC-7, gmhwxi wrote:

This one works on-line:

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats/master/doc/EXAMPLE/ATSLF/F-algebra_js.dats

On Tuesday, September 22, 2015 at 1:01:51 PM UTC-4, Aistis Raulinaitis wrote:

Beautiful! Thanks!

On Tue, Sep 22, 2015 at 7:22 AM, gmhwxi gmh...@gmail.com wrote:

For a bit fun, I get the F-algebra code running:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATSLF/F-algebra.dats

Well, it must be a bit crazy to program like this

On Tuesday, September 22, 2015 at 9:01:38 AM UTC-4, gmhwxi wrote:

Here is something that typechecks:

(* ****** ****** )
//
infixr (->) ->>
//
typedef
->> (a:type, b:type) = a - b
//
( ****** ****** *)

sortdef
ftype = type → type
typedef
Algebra (f:ftype, a:type) = f(a) ->> a

(* ****** ****** )
//
extern
fun Map{f:ftype}{a,b:type} (a ->> b): f a ->> f b
//
( ****** ****** *)

(*
datatype
Fix (f:type → type) = Iso of @{ invIso = f (Fix f) }
*)

abstype
Fix(f:type → type)
extern fun Fix_unfold{f:ftype} : Fix(f) → f (Fix(f))

(* ****** ****** )
//
fun
cata{f:ftype}{a:type}
(alg: Algebra (f,a)): (Fix f ->> a) =
lam (f: Fix(f)) => alg(Map(cata(alg))(Fix_unfold(f)))
//
( ****** ****** *)

On Tuesday, September 22, 2015 at 12:12:19 AM UTC-4, Aistis Raulinaitis wrote:

Implementing F-Algebras in ATS, wondering what I’m doing wrong or
where should I be looking? So far I have:

datatype Algebra (f:t@ype → t@ype,a:t@ype) = Algebra of (f a)

datatype Fix (f:t@ype → t@ype) = Iso of @{ invIso = f (Fix f) }

fun cata {f:t@ype → t@ype}{a:t@ype} (alg:Algebra (f,a)): (Fix f → a)
= lam (f) => alg (map (cata alg) (f.invIso))

The last line does compile, says that map is out of scope. Where would
I get it? Mind you, f is a Functor.

–
You received this message because you are subscribed to a topic in the
Google Groups “ats-lang-users” group.
To unsubscribe from this topic, visit
https://groups.google.com/d/topic/ats-lang-users/tfEnAR2vIOA/unsubscribe
.
To unsubscribe from this group and all its topics, send an email to
ats-lang...@googlegroups.com.
To post to this group, send email to ats-l...@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/28a6f4f6-a0ee-4065-a5cb-b3bfa34a36c3%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/28a6f4f6-a0ee-4065-a5cb-b3bfa34a36c3%40googlegroups.com?utm_medium=email&utm_source=footer
.

gmhwxi · September 22, 2015, 1:01pm

Here is something that typechecks:

(* ****** ****** )
//
infixr (->) ->>
//
typedef
->> (a:type, b:type) = a - b
//
( ****** ****** *)

sortdef
ftype = type → type
typedef
Algebra (f:ftype, a:type) = f(a) ->> a

(* ****** ****** )
//
extern
fun Map{f:ftype}{a,b:type} (a ->> b): f a ->> f b
//
( ****** ****** *)

(*
datatype
Fix (f:type → type) = Iso of @{ invIso = f (Fix f) }
*)

abstype
Fix(f:type → type)
extern fun Fix_unfold{f:ftype} : Fix(f) → f (Fix(f))

(* ****** ****** )
//
fun
cata{f:ftype}{a:type}
(alg: Algebra (f,a)): (Fix f ->> a) =
lam (f: Fix(f)) => alg(Map(cata(alg))(Fix_unfold(f)))
//
( ****** ****** *)On Tuesday, September 22, 2015 at 12:12:19 AM UTC-4, Aistis Raulinaitis wrote:

Implementing F-Algebras in ATS, wondering what I’m doing wrong or where
should I be looking? So far I have:

datatype Algebra (f:t@ype → t@ype,a:t@ype) = Algebra of (f a)

datatype Fix (f:t@ype → t@ype) = Iso of @{ invIso = f (Fix f) }

fun cata {f:t@ype → t@ype}{a:t@ype} (alg:Algebra (f,a)): (Fix f → a) =
lam (f) => alg (map (cata alg) (f.invIso))

The last line does compile, says that map is out of scope. Where would I
get it? Mind you, f is a Functor.

gmhwxi · September 25, 2015, 2:30am

I studied this cata-example a bit more.

As it stands now, this implementation is terribly slow.

I would like to suggest the following style of template-based
implementation of cata:

github.com

githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/TESTATS/catamorph.dats

//
// A simple example of catamorphism
//
// Author: Hongwei Xi
// Authoremail: gmhwxiATgmailDOTcom
// Start time: the 24th of September, 2015
//
(* ****** ****** *)
//
#include "share/atspre_staload.hats"
//
(* ****** ****** *)
//
datatype
expr =
| Int of int
| Add of (expr, expr)
| Mul of (expr, expr)
//
(* ****** ****** *)

This file has been truncated. show original

I think it is quite involved to get the Haskell code (implementing
F-algebra) to run efficiently.
Cata(map) is clearly defined recursively and compiling it into efficient
code likely needs to have
deforestation optimization turned on.

The template-based implementation of cata in ATS does not create any trees,
and there is no ‘Fix’
clutter, either. All that is really needed for compiling the implementation
into efficient code is to inline
function calls aggressively.On Wednesday, September 23, 2015 at 1:42:36 PM UTC-4, Aistis Raulinaitis wrote:

The nice thing about F-algebras is that you can define fexpr_eval
non-recursively. It’s quite fast, a lot of performant libs in Haskell are
written in terms of F-algebras. It’s especially good for languages that
don’t handle recursion well, and a succinct way of defining ASTs.

Also, you can simplify fix_unfold:

extern fun fix_unfold {f:ftype} : Fix f → f (Fix f)
implement fix_unfold (Fx f) = f

On Tuesday, September 22, 2015 at 10:41:05 AM UTC-7, gmhwxi wrote:

This one works on-line:

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats/master/doc/EXAMPLE/ATSLF/F-algebra_js.dats

On Tuesday, September 22, 2015 at 1:01:51 PM UTC-4, Aistis Raulinaitis wrote:

Beautiful! Thanks!

On Tue, Sep 22, 2015 at 7:22 AM, gmhwxi gmh...@gmail.com wrote:

For a bit fun, I get the F-algebra code running:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATSLF/F-algebra.dats

Well, it must be a bit crazy to program like this

On Tuesday, September 22, 2015 at 9:01:38 AM UTC-4, gmhwxi wrote:

Here is something that typechecks:

(* ****** ****** )
//
infixr (->) ->>
//
typedef
->> (a:type, b:type) = a - b
//
( ****** ****** *)

sortdef
ftype = type → type
typedef
Algebra (f:ftype, a:type) = f(a) ->> a

(* ****** ****** )
//
extern
fun Map{f:ftype}{a,b:type} (a ->> b): f a ->> f b
//
( ****** ****** *)

(*
datatype
Fix (f:type → type) = Iso of @{ invIso = f (Fix f) }
*)

abstype
Fix(f:type → type)
extern fun Fix_unfold{f:ftype} : Fix(f) → f (Fix(f))

(* ****** ****** )
//
fun
cata{f:ftype}{a:type}
(alg: Algebra (f,a)): (Fix f ->> a) =
lam (f: Fix(f)) => alg(Map(cata(alg))(Fix_unfold(f)))
//
( ****** ****** *)

On Tuesday, September 22, 2015 at 12:12:19 AM UTC-4, Aistis Raulinaitis wrote:

Implementing F-Algebras in ATS, wondering what I’m doing wrong or
where should I be looking? So far I have:

datatype Algebra (f:t@ype → t@ype,a:t@ype) = Algebra of (f a)

datatype Fix (f:t@ype → t@ype) = Iso of @{ invIso = f (Fix f) }

fun cata {f:t@ype → t@ype}{a:t@ype} (alg:Algebra (f,a)): (Fix f → a
) = lam (f) => alg (map (cata alg) (f.invIso))

The last line does compile, says that map is out of scope. Where
would I get it? Mind you, f is a Functor.

–
You received this message because you are subscribed to a topic in the
Google Groups “ats-lang-users” group.
To unsubscribe from this topic, visit
https://groups.google.com/d/topic/ats-lang-users/tfEnAR2vIOA/unsubscribe
.
To unsubscribe from this group and all its topics, send an email to
ats-lang...@googlegroups.com.
To post to this group, send email to ats-l...@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/28a6f4f6-a0ee-4065-a5cb-b3bfa34a36c3%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/28a6f4f6-a0ee-4065-a5cb-b3bfa34a36c3%40googlegroups.com?utm_medium=email&utm_source=footer
.

Aistis_Raulinaitis · September 23, 2015, 5:59pm

Also:

extern fun fexpr_eval : Algebra (Fexpr, int)

Sorry for the triple post!

So in all:

sortdef ftype = t@ype → t@ype

typedef Functor (f:ftype) = {a,b:t@ype} (a → b) → f a → f b

typedef Algebra (f:ftype, a:t@ype) = f a → a

datatype Fix (f:ftype) = Fx of f (Fix f)

extern fun fix_unfold {f:ftype} : Fix f → f (Fix f)
implement fix_unfold (Fx f) = f

extern fun cata : {f:ftype} {a:t@ype} Functor f → Algebra (f, a) → (Fix f
→ a)
implement cata map = lam alg => lam f => alg (map (cata map alg) (fix_unfold
f))

datatype Fexpr (a:t@ype)
= Int of int
| Add of (a, a)
| Mul of (a, a)

typedef Expr = Fix Fexpr

extern val fexpr_map : Functor Fexpr
implement fexpr_map f = lam e0 => ( case+ e0 of
| Int i => Int i
| Add (a, b) => Add (f a, f b)
| Mul (a, b) => Mul (f a, f b))

extern fun fexpr_eval : Algebra (Fexpr, int)
implement fexpr_eval e0 = ( case+ e0 of
| Int i => i
| Add (a, b) => a + b
| Mul (a, b) => a * b)

val I1 = Fx (Int 1) : Expr
val I2 = Fx (Int 2) : Expr
val I3 = Fx (Int 3) : Expr
val Mul_2_3 = Fx (Mul (I2, I3)) : Expr
val Add_1_Mul_2_3 = Fx (Add (I1, Mul_2_3)) : Expr

val Ans = cata fexpr_map fexpr_eval Add_1_Mul_2_3

val () = println! ("eval(1+2*3) = ", Ans)

implement main0 () = ()On Monday, September 21, 2015 at 9:12:19 PM UTC-7, Aistis Raulinaitis wrote:

Implementing F-Algebras in ATS, wondering what I’m doing wrong or where
should I be looking? So far I have:

datatype Algebra (f:t@ype → t@ype,a:t@ype) = Algebra of (f a)

datatype Fix (f:t@ype → t@ype) = Iso of @{ invIso = f (Fix f) }

fun cata {f:t@ype → t@ype}{a:t@ype} (alg:Algebra (f,a)): (Fix f → a) =
lam (f) => alg (map (cata alg) (f.invIso))

The last line does compile, says that map is out of scope. Where would I
get it? Mind you, f is a Functor.

gmhwxi · September 26, 2015, 10:57am

See the following link for some explanation on $d2ctype:

Redirecting to Google Groups Friday, September 25, 2015 at 11:45:19 PM UTC-4, Aistis Raulinaitis wrote:

Interesting, what does $d2ctype do?

On Fri, Sep 25, 2015 at 8:13 PM, Hongwei Xi <gmh...@gmail.com <javascript:>> wrote:

This is due to a new feature ($d2ctype) being used in this example.

I have just uploaded a modified version that does not use this new
feature.

On Fri, Sep 25, 2015 at 11:01 PM, Aistis Raulinaitis <sheg...@gmail.com <javascript:>> wrote:

The typechecker complains with:

patsopt -tc -d
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
639(line=50, offs=7) – 647(line=50, offs=15): error(parsing): the
syntactic entity [s0taq] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
639(line=50, offs=7) – 647(line=50, offs=15): error(parsing): the
syntactic entity [si0de] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
639(line=50, offs=7) – 647(line=50, offs=15): error(parsing): the
syntactic entity [s0exp] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
637(line=50, offs=5) – 638(line=50, offs=6): error(parsing): the keyword
[=] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
629(line=49, offs=1) – 632(line=49, offs=4): error(parsing): the keyword
‘}’ is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
610(line=46, offs=17) – 613(line=46, offs=20): error(parsing): the
syntactic entity [d0exp] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
573(line=44, offs=1) – 582(line=44, offs=10): error(parsing): the token is
discarded.
exit(ATS): uncaught exception:
_2home_2hwxi_2research_2Postiats_2git_2src_2pats_error_2esats__FatalErrorExn(1025)

Compilation exited abnormally with code 1 at Fri Sep 25 19:57:55

On Thursday, September 24, 2015 at 7:30:29 PM UTC-7, gmhwxi wrote:

I studied this cata-example a bit more.

As it stands now, this implementation is terribly slow.

I would like to suggest the following style of template-based
implementation of cata:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/TESTATS/catamorph.dats

I think it is quite involved to get the Haskell code (implementing
F-algebra) to run efficiently.
Cata(map) is clearly defined recursively and compiling it into
efficient code likely needs to have
deforestation optimization turned on.

The template-based implementation of cata in ATS does not create any
trees, and there is no ‘Fix’
clutter, either. All that is really needed for compiling the
implementation into efficient code is to inline
function calls aggressively.

On Wednesday, September 23, 2015 at 1:42:36 PM UTC-4, Aistis Raulinaitis wrote:

The nice thing about F-algebras is that you can define fexpr_eval
non-recursively. It’s quite fast, a lot of performant libs in Haskell are
written in terms of F-algebras. It’s especially good for languages that
don’t handle recursion well, and a succinct way of defining ASTs.

Also, you can simplify fix_unfold:

extern fun fix_unfold {f:ftype} : Fix f → f (Fix f)
implement fix_unfold (Fx f) = f

On Tuesday, September 22, 2015 at 10:41:05 AM UTC-7, gmhwxi wrote:

This one works on-line:

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats/master/doc/EXAMPLE/ATSLF/F-algebra_js.dats

On Tuesday, September 22, 2015 at 1:01:51 PM UTC-4, Aistis Raulinaitis wrote:

Beautiful! Thanks!

On Tue, Sep 22, 2015 at 7:22 AM, gmhwxi gmh...@gmail.com wrote:

For a bit fun, I get the F-algebra code running:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATSLF/F-algebra.dats

Well, it must be a bit crazy to program like this

On Tuesday, September 22, 2015 at 9:01:38 AM UTC-4, gmhwxi wrote:

Here is something that typechecks:

(* ****** ****** )
//
infixr (->) ->>
//
typedef
->> (a:type, b:type) = a - b
//
( ****** ****** *)

sortdef
ftype = type → type
typedef
Algebra (f:ftype, a:type) = f(a) ->> a

(* ****** ****** )
//
extern
fun Map{f:ftype}{a,b:type} (a ->> b): f a ->> f b
//
( ****** ****** *)

(*
datatype
Fix (f:type → type) = Iso of @{ invIso = f (Fix f) }
*)

abstype
Fix(f:type → type)
extern fun Fix_unfold{f:ftype} : Fix(f) → f (Fix(f))

(* ****** ****** )
//
fun
cata{f:ftype}{a:type}
(alg: Algebra (f,a)): (Fix f ->> a) =
lam (f: Fix(f)) => alg(Map(cata(alg))(Fix_unfold(f)))
//
( ****** ****** *)

On Tuesday, September 22, 2015 at 12:12:19 AM UTC-4, Aistis Raulinaitis wrote:

Implementing F-Algebras in ATS, wondering what I’m doing wrong or
where should I be looking? So far I have:

datatype Algebra (f:t@ype → t@ype,a:t@ype) = Algebra of (f a)

datatype Fix (f:t@ype → t@ype) = Iso of @{ invIso = f (Fix f) }

fun cata {f:t@ype → t@ype}{a:t@ype} (alg:Algebra (f,a)): (Fix f
→ a) = lam (f) => alg (map (cata alg) (f.invIso))

The last line does compile, says that map is out of scope. Where
would I get it? Mind you, f is a Functor.

–
You received this message because you are subscribed to a topic in
the Google Groups “ats-lang-users” group.
To unsubscribe from this topic, visit
https://groups.google.com/d/topic/ats-lang-users/tfEnAR2vIOA/unsubscribe
.
To unsubscribe from this group and all its topics, send an email to
ats-lang...@googlegroups.com.
To post to this group, send email to ats-l...@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/28a6f4f6-a0ee-4065-a5cb-b3bfa34a36c3%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/28a6f4f6-a0ee-4065-a5cb-b3bfa34a36c3%40googlegroups.com?utm_medium=email&utm_source=footer
.

–
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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
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/a59e0bc4-6148-4e0f-bab8-b2a7b2104bc5%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/a59e0bc4-6148-4e0f-bab8-b2a7b2104bc5%40googlegroups.com?utm_medium=email&utm_source=footer
.

–
You received this message because you are subscribed to a topic in the
Google Groups “ats-lang-users” group.
To unsubscribe from this topic, visit
https://groups.google.com/d/topic/ats-lang-users/tfEnAR2vIOA/unsubscribe.
To unsubscribe from this group and all its topics, send an email to
ats-lang...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
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/CAPPSPLqU6hSBn9mmjRpoy%3DXA1rZq8YMvzWYkMnfB7uuSu73AAA%40mail.gmail.com
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLqU6hSBn9mmjRpoy%3DXA1rZq8YMvzWYkMnfB7uuSu73AAA%40mail.gmail.com?utm_medium=email&utm_source=footer
.

gmhwxi · September 22, 2015, 2:22pm

For a bit fun, I get the F-algebra code running:

github.com

githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATSLF/F-algebra.dats

(* ****** ****** *)
//
// HX-2015-09-22
//
// Please visit the link:
// https://groups.google.com/forum/#!topic/ats-lang-users/tfEnAR2vIOA
//
(* ****** ****** *)
//
#include "share/atspre_staload.hats"
//
(* ****** ****** *)
//
infixr (->) ->>
//
typedef
->> (a:type, b:type) = a -<cloref1> b
//
(* ****** ****** *)

This file has been truncated. show original

Well, it must be a bit crazy to program like this :)On Tuesday, September 22, 2015 at 9:01:38 AM UTC-4, gmhwxi wrote:

Here is something that typechecks:

(* ****** ****** )
//
infixr (->) ->>
//
typedef
->> (a:type, b:type) = a - b
//
( ****** ****** *)

sortdef
ftype = type → type
typedef
Algebra (f:ftype, a:type) = f(a) ->> a

(* ****** ****** )
//
extern
fun Map{f:ftype}{a,b:type} (a ->> b): f a ->> f b
//
( ****** ****** *)

(*
datatype
Fix (f:type → type) = Iso of @{ invIso = f (Fix f) }
*)

abstype
Fix(f:type → type)
extern fun Fix_unfold{f:ftype} : Fix(f) → f (Fix(f))

(* ****** ****** )
//
fun
cata{f:ftype}{a:type}
(alg: Algebra (f,a)): (Fix f ->> a) =
lam (f: Fix(f)) => alg(Map(cata(alg))(Fix_unfold(f)))
//
( ****** ****** *)

On Tuesday, September 22, 2015 at 12:12:19 AM UTC-4, Aistis Raulinaitis wrote:

Implementing F-Algebras in ATS, wondering what I’m doing wrong or where
should I be looking? So far I have:

datatype Algebra (f:t@ype → t@ype,a:t@ype) = Algebra of (f a)

datatype Fix (f:t@ype → t@ype) = Iso of @{ invIso = f (Fix f) }

fun cata {f:t@ype → t@ype}{a:t@ype} (alg:Algebra (f,a)): (Fix f → a) =
lam (f) => alg (map (cata alg) (f.invIso))

The last line does compile, says that map is out of scope. Where would I
get it? Mind you, f is a Functor.

Aistis_Raulinaitis · September 26, 2015, 3:01am

The typechecker complains with:

patsopt -tc -d
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
639(line=50, offs=7) – 647(line=50, offs=15): error(parsing): the
syntactic entity [s0taq] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
639(line=50, offs=7) – 647(line=50, offs=15): error(parsing): the
syntactic entity [si0de] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
639(line=50, offs=7) – 647(line=50, offs=15): error(parsing): the
syntactic entity [s0exp] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
637(line=50, offs=5) – 638(line=50, offs=6): error(parsing): the keyword
[=] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
629(line=49, offs=1) – 632(line=49, offs=4): error(parsing): the keyword
‘}’ is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
610(line=46, offs=17) – 613(line=46, offs=20): error(parsing): the
syntactic entity [d0exp] is needed.
/home/aistis/Projects/github/ATS-Postiats/doc/EXAMPLE/TESTATS/catamorph.dats:
573(line=44, offs=1) – 582(line=44, offs=10): error(parsing): the token is
discarded.
exit(ATS): uncaught exception:
_2home_2hwxi_2research_2Postiats_2git_2src_2pats_error_2esats__FatalErrorExn(1025)

Compilation exited abnormally with code 1 at Fri Sep 25 19:57:55On Thursday, September 24, 2015 at 7:30:29 PM UTC-7, gmhwxi wrote:

I studied this cata-example a bit more.

As it stands now, this implementation is terribly slow.

I would like to suggest the following style of template-based
implementation of cata:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/TESTATS/catamorph.dats

I think it is quite involved to get the Haskell code (implementing
F-algebra) to run efficiently.
Cata(map) is clearly defined recursively and compiling it into efficient
code likely needs to have
deforestation optimization turned on.

The template-based implementation of cata in ATS does not create any
trees, and there is no ‘Fix’
clutter, either. All that is really needed for compiling the
implementation into efficient code is to inline
function calls aggressively.

On Wednesday, September 23, 2015 at 1:42:36 PM UTC-4, Aistis Raulinaitis wrote:

The nice thing about F-algebras is that you can define fexpr_eval
non-recursively. It’s quite fast, a lot of performant libs in Haskell are
written in terms of F-algebras. It’s especially good for languages that
don’t handle recursion well, and a succinct way of defining ASTs.

Also, you can simplify fix_unfold:

extern fun fix_unfold {f:ftype} : Fix f → f (Fix f)
implement fix_unfold (Fx f) = f

On Tuesday, September 22, 2015 at 10:41:05 AM UTC-7, gmhwxi wrote:

This one works on-line:

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats/master/doc/EXAMPLE/ATSLF/F-algebra_js.dats

On Tuesday, September 22, 2015 at 1:01:51 PM UTC-4, Aistis Raulinaitis wrote:

Beautiful! Thanks!

On Tue, Sep 22, 2015 at 7:22 AM, gmhwxi gmh...@gmail.com wrote:

For a bit fun, I get the F-algebra code running:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATSLF/F-algebra.dats

Well, it must be a bit crazy to program like this

On Tuesday, September 22, 2015 at 9:01:38 AM UTC-4, gmhwxi wrote:

Here is something that typechecks:

(* ****** ****** )
//
infixr (->) ->>
//
typedef
->> (a:type, b:type) = a - b
//
( ****** ****** *)

sortdef
ftype = type → type
typedef
Algebra (f:ftype, a:type) = f(a) ->> a

(* ****** ****** )
//
extern
fun Map{f:ftype}{a,b:type} (a ->> b): f a ->> f b
//
( ****** ****** *)

(*
datatype
Fix (f:type → type) = Iso of @{ invIso = f (Fix f) }
*)

abstype
Fix(f:type → type)
extern fun Fix_unfold{f:ftype} : Fix(f) → f (Fix(f))

(* ****** ****** )
//
fun
cata{f:ftype}{a:type}
(alg: Algebra (f,a)): (Fix f ->> a) =
lam (f: Fix(f)) => alg(Map(cata(alg))(Fix_unfold(f)))
//
( ****** ****** *)

On Tuesday, September 22, 2015 at 12:12:19 AM UTC-4, Aistis Raulinaitis wrote:

Implementing F-Algebras in ATS, wondering what I’m doing wrong or
where should I be looking? So far I have:

datatype Algebra (f:t@ype → t@ype,a:t@ype) = Algebra of (f a)

datatype Fix (f:t@ype → t@ype) = Iso of @{ invIso = f (Fix f) }

fun cata {f:t@ype → t@ype}{a:t@ype} (alg:Algebra (f,a)): (Fix f →
a) = lam (f) => alg (map (cata alg) (f.invIso))

The last line does compile, says that map is out of scope. Where
would I get it? Mind you, f is a Functor.

–
You received this message because you are subscribed to a topic in the
Google Groups “ats-lang-users” group.
To unsubscribe from this topic, visit
https://groups.google.com/d/topic/ats-lang-users/tfEnAR2vIOA/unsubscribe
.
To unsubscribe from this group and all its topics, send an email to
ats-lang...@googlegroups.com.
To post to this group, send email to ats-l...@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/28a6f4f6-a0ee-4065-a5cb-b3bfa34a36c3%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/28a6f4f6-a0ee-4065-a5cb-b3bfa34a36c3%40googlegroups.com?utm_medium=email&utm_source=footer
.

Topic		Replies	Views
Typechecking Error Google Group	2	336	March 26, 2014
Recursive dataviewtype with array Google Group	3	330	July 26, 2013
Try Out Oneboxed URL Playground	2	1054	September 2, 2016
Operator resolution Google Group	16	540	July 11, 2013
Polymorphic datatype Google Group	8	368	June 5, 2013

Fuctorial map

Related Topics