Memoization in Type Calculation

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Memoization in Type Calculation

Dmitry Olshansky
Hello, cafe!

I wonder is there some possibility to get Memoization in Type Calculation (e.g. in closed Type Families)?

Can we make something more efficient for famous Fib function then

type family Fib (n::Nat) :: Nat where
  Fib 1 = 1
  Fib 2 = 1
  Fib n = Fib (n-1) + Fib (n-2)

This Fib has obviously exponential calculation time and we need some memoization.

If it is impossible right now, maybe there is a ticket for this? It seems to me very important things, no?

Probably in this case we can write TypeChecker Plugin, but it looks like the common problem.

Best regards,
Dmitry




_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Memoization in Type Calculation

Rahul Muttineni
Hi Dmitry,

You can effectively think of the type-level language of Haskell as a strict functional language with almost no syntactic sugar, and recursion is the *only* way of getting the behaviour of a loop. The best you can do to improve the performance of that type family is to write it in tail-recursive form using a helper function and which will make the type family reduction look more linear vs a tree like it is now and make it easier for the type checker to quickly spit out the result.

type family Fib (n::Nat) :: Nat where
  Fib n = GoFib 0 1 n

type family GoFib (a :: Nat) (b :: Nat) (n :: Nat) where
  GoFib a _ 0 = a
  GoFib a b n = GoFib b (a + b) (n - 1)

Hope that helps,
Rahul

On Mon, Jul 17, 2017 at 11:19 AM, Dmitry Olshansky <[hidden email]> wrote:
Hello, cafe!

I wonder is there some possibility to get Memoization in Type Calculation (e.g. in closed Type Families)?

Can we make something more efficient for famous Fib function then

type family Fib (n::Nat) :: Nat where
  Fib 1 = 1
  Fib 2 = 1
  Fib n = Fib (n-1) + Fib (n-2)

This Fib has obviously exponential calculation time and we need some memoization.

If it is impossible right now, maybe there is a ticket for this? It seems to me very important things, no?

Probably in this case we can write TypeChecker Plugin, but it looks like the common problem.

Best regards,
Dmitry




_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.



--
Rahul Muttineni

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Fwd: Memoization in Type Calculation

Dmitry Olshansky
Rahul, thanks! It is really simple!

2017-07-17 21:33 GMT+03:00 Rahul Muttineni <[hidden email]>:
Hi Dmitry,

You can effectively think of the type-level language of Haskell as a strict functional language with almost no syntactic sugar, and recursion is the *only* way of getting the behaviour of a loop. The best you can do to improve the performance of that type family is to write it in tail-recursive form using a helper function and which will make the type family reduction look more linear vs a tree like it is now and make it easier for the type checker to quickly spit out the result.

type family Fib (n::Nat) :: Nat where
  Fib n = GoFib 0 1 n

type family GoFib (a :: Nat) (b :: Nat) (n :: Nat) where
  GoFib a _ 0 = a
  GoFib a b n = GoFib b (a + b) (n - 1)

Hope that helps,
Rahul

On Mon, Jul 17, 2017 at 11:19 AM, Dmitry Olshansky <[hidden email]> wrote:
Hello, cafe!

I wonder is there some possibility to get Memoization in Type Calculation (e.g. in closed Type Families)?

Can we make something more efficient for famous Fib function then

type family Fib (n::Nat) :: Nat where
  Fib 1 = 1
  Fib 2 = 1
  Fib n = Fib (n-1) + Fib (n-2)

This Fib has obviously exponential calculation time and we need some memoization.

If it is impossible right now, maybe there is a ticket for this? It seems to me very important things, no?

Probably in this case we can write TypeChecker Plugin, but it looks like the common problem.

Best regards,
Dmitry




_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.



--
Rahul Muttineni



_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.