Fcf-containers - additional tools to type-level programming

Announcements
#1

Dear all,

Fcf-containers gives additional tools to do type-level programming in the fashion set by first-class-families.

Why fcf-containers? It could be used in e.g. to

  • increase the safety measures of runtime methods,
  • pre-calculate complex things once on compile time and not every time the executable is run,
  • provide users a way to choose between different algorithms for solving a problem based on problem instance properties (e.g. local vs network, or small vs large) known in advance.

Why fcf-like? The kind of signatures used for functions might be easier to read for some people and the ability to apply partially a function is very nice tool to have. The techniques that allows this are defunctionalization, encoding the functions with empty data types and the use of open type family to Eval the constructed expressions. The following is from blog-post introducing the first-class-families:

Encoding type families with type constructors allows them to be passed around without applying them, which is not possible in their original form.

The original form refers to type family declaration that has to be fully evaluated.

As an example, consider sum of Nats given in a type-level list. Fcf-containers add type-level functions so that you can calculate this even with catamorphism.

Note that the algebra is defined only at type-level. We use the type-level base functor ListF here.

data SumAlg :: Algebra (ListF Nat) Nat
type instance Eval (SumAlg 'NilF) = 0
type instance Eval (SumAlg ('ConsF a b)) = a TL.+ b

After that, we can use it on ghci with the provided Cata-morphism

> :kind! Eval (Cata SumAlg =<< ListToFix '[1,2,3,4])
> = 10

Or, if you like AoC problems, there is one example showing how to calculate something on type-level and use the result (see orbits example).

In addition to the motivation given above, and because finding and laying out good reasons is hard, if you find out some, could you please e.g. drop and show those here?

This is my first ever published package so I’d like to welcome any feedback you may have.

3 Likes
#2

(editorial note: I think you’ve got your link text and url backwards on the markdown for your post! :slight_smile: )

1 Like
#3

Thank you very much! Now the links should be ok. My next challenge is to get the CI to work at github and will look into that later today :slight_smile:

#4

I’m happy to announce version 0.2.0 of fcf-containers is now on Hackage. It uses the just released first-class-families 0.7.0.

Other additions include things like

  • travis build and tests for 8.2.2, 8.4.4, 8.6.5 and 8.8.1
  • Fcf.Data.Symbol -module
  • additions to Fcf.Data.Set -module

Here is an example about one added PowerSet-function. On ghci, first form a type-level Set containing elements 1, 2, and 3 and feed it to the PowerSet-function:

> :kind! Eval (PowerSet =<< FromList '[1,2,3])

The result is:

= 'Set
    '[ 'Set '[], 'Set '[3], 'Set '[2], 'Set '[2, 3], 'Set '[1],
       'Set '[1, 2], 'Set '[1, 3], 'Set '[1, 2, 3]]

Note that the current implementation uses gray codes, so the order is not lexicographic.

#5

I’m happy to announce version 0.3.0 of fcf-containers is now on Hackage.

This version adds functions into Set, List and Symbol modules, does some small scale re-organization etc.

This also adds a new example, which show how to use utilities meant for processing Symbols, Lists, type-level Map-structure among other things, please do take a look of Haiku.hs

Shortly, the example first defines a vocabulary

data HaikuWords :: Exp [[Text]]
type instance Eval HaikuWords =
    '[ '[ 'Text '["a","a"], 'Text '["m","u"]]
     , '[ 'Text '["a","a"], 'Text '["m","u","l"], 'Text '["l","a"]]
     , '[ 'Text '["a"], 'Text '["j","a"], 'Text '["t","u","s"]]
     , '[ 'Text '["j","o"], 'Text '["k","i","n"]]
     , '[ 'Text '["k","i","e"], 'Text '["l","i"]]
     , '[ 'Text '["l","o","i"], 'Text '["k","o","i"], 'Text '["l","e"], 'Text '["v","a"]]
     , '[ 'Text '["m","u","u"]]
     , '[ 'Text '["v","a","n"], 'Text '["h","e"], 'Text '["n","e","e"]]
     , '[ 'Text '["u","u"], 'Text '["s","i"]]
     ]

and then a Haiku. We want to check that Haiku follows the syllable structure

data Haiku :: Exp Text
type instance Eval Haiku =
    'Text '[ "k","i","e","l","i"," ","v","a","n","h","e","n","e","e","\n"
           , "l","o","i","k","o","i","l","e","v","a"," ","a","j","a","t","u","s","\n"
           , "a","a","m","u","l","l","a"," ","u","u","s","i"
           -- , "j","o", "k","i","n" -- test with clearly wrong input (won't compile)
           ]

… so after couple of type-level functions we are ready to do the check and if it compiles, print it:

showHaiku
    :: forall symbol. (symbol ~ Eval (ToSymbol =<< Haiku), 'True ~ Eval CheckHaiku)
    => String
showHaiku = TL.symbolVal @symbol Proxy
1 Like
#6

I’m happy to announce that version 0.4.0 of fcf-containers is now available on Hackage.

This version adds NatMap that corresponds to IntMap in the containers. Further, we also add Para and Histo with examples.

:kind! Eval (FibHisto 100)
Eval (FibHisto 100) :: Nat
= 354224848179261915075

Quick comparison with the slides Recursion Schemes by Example by Tim Williams says that the figures looks close to each other. Further, this calculates the 500th fibonacci in reasonable time etc.