Fuctorial map

[Aistis Raulinaitis]

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]

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..

[gmhwxi]

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

https://github.com/githwxi/ATS-Postiats/tree/master/doc/EXAMPLE/ATSLF

I remember that I had to use type instead of t@ype.

[gmhwxi]

Here is something that typechecks:

(* ****** ****** *)
//
infixr (->) ->>
//
typedef
->> (a:type, b:type) = a -<cloref1> 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)))
//
(* ****** ****** *)

[gmhwxi]

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 :)

[Aistis Raulinaitis]

Beautiful! Thanks!

--
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.

[gmhwxi]

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

[Aistis Raulinaitis]

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 () = ()

[Aistis Raulinaitis]

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:

[Aistis Raulinaitis]

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:

[gmhwxi]

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.

[gmhwxi]

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.

[Aistis Raulinaitis]

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

[Hongwei Xi]

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.

--
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.

[Aistis Raulinaitis]

Interesting, what does $d2ctype do?

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLqU6hSBn9mmjRpoy%3DXA1rZq8YMvzWYkMnfB7uuSu73AAA%40mail.gmail.com.

[gmhwxi]

See the following link for some explanation on $d2ctype:

https://groups.google.com/forum/#!topic/ats-lang-users/lK9WrvIT5i8

[gmhwxi]

This is about functorial map:

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