Skip to content

Latest commit

 

History

History
678 lines (441 loc) · 14.5 KB

20230111_hhslides.md

File metadata and controls

678 lines (441 loc) · 14.5 KB

Slide

Preliminary Intro to Defunctionalization

Slides for Helsinki Haskell Meetup 11.1.2023.

These slides can be found at /~https://github.com/gspia/fcf-containers. Some of the code examples can be found under directory examples with name 20230111_hhmeetup.hs.

Slide

Defunctionalization

"defunctionalization is a compile-time transformation which eliminates higher-order functions, replacing them by a single first-order apply function. The technique was first described by John C. Reynolds in his 1972 paper..."

On Haskell, the defunctionalization can refer to both type-level computation technique as well as computations done on run-time. Please, do take a look of that wiki page for the example of the latter.

In this presentation, we focus mainly on type-level computations.

Slide

Resources

Thinking With Types book has a chapter about on this technique:

Lysxia's blog posts:

Lysxia gives the basic definitions and examples. There are four other, related libs that build on his first-class-families lib.

IcelandJack's gist:

Examples of different techniques that may or may not be helpful when writing type-level functions.

Slide

Libs

It is worth taking a look at the source code:

Both of the above libs contain several smaller examples implemented as doc tests. They can be run on ghci. Fcf-containers also has couple of "larger" examples showing, how to solve some random problems.

To see and understand the example, you need to look at the code. Some of the symbols can be seen when looking at the haddocks but not the actual definitions, what they do (maybe the names are descriptive enough, like "Plus2" or "PureXPlusY").

Slide

Related work

Singletons library

https://hackage.haskell.org/package/singletons /~https://github.com/goldfirere/singletons

uses also the very similar or same technique. The notation is a bit different.

The main difference between the libs on prev page and singletons is that singletons uses a lot of template haskell and is meant (among other things) to help automate turning value level function to type level function. Fcf libs in turn, require writing the type level functions "in pieces".

Sometimes, it can be difficult to see, why a particular value level construct is not working directly on type level. When implementing the function "manually", it is easier to debug and understand the problematic cases.

Thus, even if you turn out to using singletons way of writing the type level functions and defunctionalization, it might be a good idea to do and learn on how to write those functions from "ground-up".

On singletons and how the defunctionalization is described there, see: https://typesandkinds.wordpress.com/2013/04/01/defunctionalization-for-the-win/

Slide

What can you do? Why?

Maybe rather ask, what do you know in advance of your problem?

What is known at the compile time?

Do you need to guarantee or just handle non-trivial properties at type level?

Slide

A word of warning

Doing extensively type level programming just introduces an another level of bugs... The type level guarantees of type level programming, sigh.

You still need to test the code, including the type level function. Further, there is still a need to understand the requirements.

This becomes very pronounced especially on cases, where writing libs that are meant to provide safe-to-use features on value level.

Slide

Type level functions, one way

Type families are used to define type level functions. They are evaluated strictly and they need to "saturate".

Then we face problems: how to pass functions to other functions? Can we define something lazily?

For example, the following is a type-level fst:

type family   Fst' (xy :: (a, b)) :: a
type instance Fst' '(x, y) = x

Let's try it:

> :kind! Fst' '(Int,Char)
Fst' '(Int,Char) :: *
= Int

Slide

Basic definition

From Lysxia

...will be replaced with this data type Fst where the type constructor represents the Fst' type family, together with a type instance clause for a single general type family, called Eval:

--   fst ::     (a, b)  ->     a
data Fst (xy :: (a, b)) :: Exp a
type instance Eval (Fst '(x, y)) = x

...type family Eval evaluates applied type families. More generally, we will see that Eval can also work with complex expressions, hence the name of the kind Exp.

type family Eval (e :: Exp a) :: a

The kind Exp a of an expression is indexed by the kind a of the result of its evaluation. The kind of expressions Exp is actually defined as:

type Exp a = a -> Type

Slide

Let's try the first-class-families lib, it contains the Fst example of previous slide:

> :kind! Eval (Fst '(Int, Char))
Eval (Fst '(Int, Char)) :: *
= Int

Map works for some types:

> :kind! Eval (Map Fst '[ '(Char, Int), '(Int,String) ])
Eval (Map Fst '[ '(Char, Int), '(Int,String) ]) :: [*]
= '[Char, Int]
> :kind! Eval (Map Fst '[ '(2, 3), '(5,6) ])
Eval (Map Fst '[ '(2, 3), '(5,6) ]) :: [Nat]
= '[2, 5]

The above one does not work with Fst'.

Also, how to combine Nat's and other types? (Not that easy and requires some extra effort.)

Slide

List of lists

data MapFst :: [(a,b)] -> Exp [a]
type instance Eval (MapFst a) = Eval (Map Fst a)

:kind! Eval (MapFst '[ '(2,3), '(5,6)])
Eval (MapFst '[ '(2,3), '(5,6)]) :: [Nat]
= '[2, 5]

> :kind! Eval (Map MapFst '[ '[ '(4,3), '(5,7)]])
Eval (Map MapFst '[ '[ '(4,3), '(5,7)]]) :: [[Nat]]
= '[ '[4, 5]]

Or just

> :kind! Eval (Map (Map Fst) '[ '[ '(4,3), '(5,7)]])
Eval (Map (Map Fst) '[ '[ '(4,3), '(5,7)]]) :: [[Nat]]
= '[ '[4, 5]]

Slide

How about composing functions (the "dot")?

We need to use (=<<) from FcF for that.

> :kind! Eval (Head =<< (Map (Map Fst) '[ '[ '(4,3), '(5,7)]]))
Eval (Head =<< (Map (Map Fst) '[ '[ '(4,3), '(5,7)]])) :: Maybe
                                                            [Nat]
= 'Just '[4, 5]

or

> :kind! Eval (FromMaybe 1 =<< Head =<< FromMaybe '[1] =<< Head =<< (Map (Map Fst) '[ '[ '(4,3), '(5,7)]]))
Eval (FromMaybe 1 =<< Head =<< FromMaybe '[1] =<< Head =<< (Map (Map Fst) '[ '[ '(4,3), '(5,7)]])) :: Nat
= 4

Slide

Compare the value level

> (head . head) [[1],[2],[3]]
1

to the following type level function

> :kind! Eval (FromMaybe 0 =<< Head =<< FromMaybe '[0] =<< Head '[ '[1], '[2], '[3]])
Eval (FromMaybe 0 =<< Head =<< FromMaybe '[0] =<< Head '[ '[1], '[2], '[3]]) :: Nat
= 1

Slide

Or you can use (<=<) from Fcf.

> :kind! Eval ( (Snd <=< Fst) '( '(1,2), '(3,4)))
Eval ( (Snd <=< Fst) '( '(1,2), '(3,4))) :: Nat
= 2

> :kind! Eval ( Snd =<< Fst '( '(1,2), '(3,4)))
Eval ( Snd =<< Fst '( '(1,2), '(3,4))) :: Nat
= 2

Or the from the last slide:

> :kind! Eval ( (FromMaybe 0 <=< Head <=< FromMaybe '[0] <=< Head) '[ '[1], '[2], '[3]])
Eval ( (FromMaybe 0 <=< Head <=< FromMaybe '[0] <=< Head) '[ '[1], '[2], '[3]]) :: Nat
= 1

Slide

Functors, Applicatives, Monads

We have combinators for implementing Functors, Applicatives and even Monads.

> :kind! Eval ( (FromMaybe 0 <=< Head <=< FromMaybe '[0] <=< Head) '[ '[1], '[2], '[3]])
Eval ( (FromMaybe 0 <=< Head <=< FromMaybe '[0] <=< Head) '[ '[1], '[2], '[3]]) :: Nat
= 1
> :kind! Eval (MapM (ConstFn '[ 'True, 'False]) '[1,2,3])
Eval (MapM (ConstFn '[ 'True, 'False]) '[1,2,3]) :: [[Bool]]
= '[ '[ 'True, 'True, 'True], '[ 'True, 'True, 'False],
     '[ 'True, 'False, 'True], '[ 'True, 'False, 'False],
     '[ 'False, 'True, 'True], '[ 'False, 'True, 'False],
     '[ 'False, 'False, 'True], '[ 'False, 'False, 'False]]

> :kind! Eval (Sequence '[ '[1,2], '[3,4]])
Eval (Sequence '[ '[1,2], '[3,4]]) :: [[Nat]]
= '[ '[1, 3], '[1, 4], '[2, 3], '[2, 4]]

> :kind! Eval (Sequence '[ 'Just "a", 'Just "b"])
Eval (Sequence '[ 'Just "a", 'Just "b"]) :: Maybe
                                              [GHC.Types.Symbol]
= 'Just '["a", "b"]

Slide

More on lists

Another list example:

> import Control.Monad
> liftM2 (+) [1,2,3] [10,20]
[11,21,12,22,13,23]

And same on type level:

> :kind! Eval (LiftA2 (Fcf.+) '[1,2,3] '[10,20])
Eval (LiftA2 (Fcf.+) '[1,2,3] '[10,20]) :: [Nat]
= '[11, 21, 12, 22, 13, 23]

Slide

More on lists

Continuing with another list example:

Related example (from the code of fcf lib):

data XPlusYs :: Nat -> [Nat] -> Exp [Nat]
type instance Eval (XPlusYs x ys) = Eval (ys >>= PureXPlusY x)

-- | An example implementing
--
-- sumM xs ys = do
--     x <- xs
--     y <- ys
--     return (x + y)
--
-- or
--
-- sumM xs ys = xs >>= (\x -> ys >>= (\y -> pure (x+y)))
--
-- Note the use of helper functions. This is a bit awkward, a type level
-- lambda would be nice.
data XsPlusYsMonadic :: [Nat] -> [Nat] -> Exp [Nat]
type instance Eval (XsPlusYsMonadic xs ys) = Eval (xs >>= Flip XPlusYs ys)

Now we can write:

> :kind! Eval (XsPlusYsMonadic '[1,2,3] '[10,20])
Eval (XsPlusYsMonadic '[1,2,3] '[10,20]) :: [Nat]
= '[11, 21, 12, 22, 13, 23]

Slide

Data (structure) types, control structures

Possible, see e.g. the fcf lib for examples:

  • MapC - named this way so that it doesn't overlap with type level Map function
  • NatMap corresponds to IntMap in the containers
  • Set
  • Tree

etc. On some of the above cases, the basic implementation isn't particularly efficient at the moment. Anyhow, they give the data structure and an example on how to write data structures on type level.

The fcf lib contains also some examples on how to write different kinds of control structures and algorithms. In this presentation, we don't go into that but just ask you to take a look of the lib.

Slide

Folding

Make the type level foldl function!

It is not given in the libs, yet. We can work with the following variant:

foldl :: (b -> a -> b) -> b -> [a] -> b
foldl f init xs = foldr (flip f) init (reverse xs)
data Foldl :: (b -> a -> Exp b) -> b -> t a -> Exp b
type instance Eval (Foldl f b ta) = Eval (Foldr (Flip f) b (Reverse ta))

The above one doesn't work.

> :kind! Eval (Foldl (Fcf.+) 0 '[1,2,3])
Eval (Foldl (Fcf.+) 0 '[1,2,3]) :: Nat
= Eval (Foldl (Fcf.+) 0 '[1, 2, 3])

Slide

More on Folding

So, the not working definitions just get stuck easily.

But the following definition works. The Eval in there is easy to miss:

type instance Eval (Foldl f b ta) = Eval (Foldr (Flip f) b (Eval (Reverse ta)))
> :kind! Eval (Foldl (Fcf.+) 0 '[1,2,3])
Eval (Foldl (Fcf.+) 0 '[1,2,3]) :: Nat
= 6

Slide

Breadth-first search for trees

Let's make breadth-first search for trees, this doesn't exists directly in the libs.

Let's use this as starting point (from https://matthewmanela.com/blog/breadth-first-tree-traversal-in-haskell/)

breadth :: Show a => Tree a -> [a]
breadth nd =  map rootLabel $ nd : (breadth2 [nd])
  where
      breadth2 :: [Tree a] -> [Tree a]
      breadth2 [] = []
      breadth2 nds =
        let cs = foldr ((++) . subForest) [] nds
         in cs ++ breadth2 cs

tree :: Tree Int
tree = Node 1 [Node 2 [Node 4 [], Node 5 [Node 8 [], Node 9[]]], Node 3 [Node 6 [Node 10 []], Node 7 []]]

and then

> breadth tree
[1,2,3,4,5,6,7,8,9,10]

Slide

BFS on type level

Next, on type level. We face some difficulties and need build everything in pieces.

data CalcCS :: [Tree a] -> Exp [Tree a]
-- type instance Eval (CalcCS trs) = Eval (Foldr ((L.++) <=< GetForest) '[] trs) -- doesn't work
type instance Eval (CalcCS trs) = Eval (Foldr FoldFun '[] trs) 

data FoldFun :: Tree a -> [Tree a] -> Exp [Tree a]
type instance Eval (FoldFun a b) = Eval ( (Eval (GetForest a)) L.++ b)

data Breadth2 :: [Tree a] -> Exp [Tree a]
type instance Eval (Breadth2 '[]) = '[]
type instance Eval (Breadth2 (t ':ts)) = Eval ( (Eval (CalcCS (t ': ts))) L.++ (Eval (Breadth2 (Eval (CalcCS (t ': ts))))))

data FormTreeList :: Tree a -> Exp [Tree a]
type instance Eval (FormTreeList tr) = tr ': (Eval (Breadth2 '[tr]))

data Breadth :: Tree a -> Exp [a]
type instance Eval (Breadth tr) = Eval (Map GetRoot =<< FormTreeList tr)

Slide

Let's try our BFS

Then we can evaluate:

> :kind! Eval (Breadth (Node 1 '[Node 2 '[Node 4 '[], Node 5 '[Node 8 '[], Node 9 '[]]], Node 3 '[Node 6 '[Node 10 '[]], Node 7 '[]]]))
Eval (Breadth (Node 1 '[Node 2 '[Node 4 '[], Node 5 '[Node 8 '[], Node 9 '[]]], Node 3 '[Node 6 '[Node 10 '[]], Node 7 '[]]])) :: [Nat]
= '[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]

The implementation on prev slide might can be tidied. (To be found out.)

Slide

From type level to values

How to get the answer to value level?

answer :: forall n.
  (n ~ Eval (Breadth
     (Node 1 '[Node 2 '[Node 4 '[], Node 5 '[Node 8 '[], Node 9 '[]]]
                       , Node 3 '[Node 6 '[Node 10 '[]], Node 7 '[]]
                       ]))
  ) => [Int]
answer = natVals @n Proxy

Slide

Helpers for the prev slide

Note that for a single value or symbol, we have ready made functions. The definition of natVals was found from https://hackage.haskell.org/package/numhask-array-0.10.1/docs/src/NumHask.Array.Shape.html#natVals

class KnownNats (ns :: [Nat]) where
  natVals :: Proxy ns -> [Int]

instance KnownNats '[] where
  natVals _ = []

instance (TL.KnownNat n, KnownNats ns) => KnownNats (n : ns) where
  natVals _ = fromInteger (TL.natVal (Proxy @n)) : natVals (Proxy @ns)

Slide

Differencies to singletons lib?

Singletons has a lot of utilities for doing similar type level programming. There is Apply and it is possible to define

  • Eval in terms of Apply
  • Apply in terms of Eval

See https://blog.poisson.chat/posts/2018-08-06-one-type-family.html for details.

Also, singletons enable the other direction: how to get values to type level.