Type-level witnesses of transformations

[0xd34df00d]

We've discussed ways to ensure that all other transformations that a given one depends upon do indeed run before the given one. Preferably, at type level, so that the type also serves as a documentation.

I've been hacking a little bit on this today, and this is a proof-of-concept that I've come up with:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind

-- Tags for different transformations,
-- think 'data EtaExpanded', 'data Monomorphized' and so on.
data Foo
data Bar
data Baz

-- A set of transformation tags is basically a list of types.
type Tags = [Type]

-- A transformation on type 'a' is a function 'a -> a'
-- along with the list of tags of transformations that it requires, and a list of tags it provides.
--
-- A transformation that's ready to be run has 'requires ~ '[]',
-- which might even be made a constraint on the function executing the pipeline.
type Xform :: Tags -> Tags -> Type -> Type
newtype Xform requires provides a = Xform (a -> a)

-- Kinda-set-union that doesn't care about introducing duplicates
type family (∪) (xs :: [a]) (ys :: [a]) :: [a] where
  '[] ∪ ys = ys
  (x ': xs) ∪ ys = x ': (xs ∪ ys)

-- Deleting all copies of a given val… err, type from a list of types
type family Del (xs :: [a]) (d :: a) :: [a] where
  Del '[] _ = '[]
  Del (d ': xs) d = Del xs d
  Del (x ': xs) d = x ': Del xs d

-- Set subtraction
type family (\\) (xs :: [a]) (ys :: [a]) :: [a] where
  xs \\ '[] = xs
  xs \\ (y ': ys) = Del xs y \\ ys

-- Left-to-right composition of transformations.
-- If we apply a transformation requiring r₁ and producing p₁
-- and then apply one requiring r₂ and producing p₂,
-- the composition requires r₁ ∪ (r₂ \\ p₁) and produces p₁ ∪ p₂.
--
-- It's tedious but easy to see that this is also associative at type level too,
-- as expected.
(&) :: Xform r1 p1 a
    -> Xform r2 p2 a
    -> Xform (r1 ∪ (r2 \\ p1)) (p1 ∪ p2) a
Xform f1 & Xform f2 = Xform $ f2 . f1

-- Some examples
t11 :: Xform '[] '[ Foo ] a
t11 = Xform id

t12 :: Xform '[ Foo ] '[ Bar ] a
t12 = Xform id

t13 :: Xform '[ Bar ] '[ Baz ] a
t13 = Xform id

t1All = t11 & t12 & t13
-- ghc gladly infers
-- t1All :: Xform '[] '[Foo, Bar, Baz] a
-- indeed, this is a correct transformation that can be run

t21 :: Xform '[] '[ Foo ] a
t21 = Xform id

t22 :: Xform '[ Baz ] '[ Bar ] a
t22 = Xform id

t23 :: Xform '[ Bar ] '[ Baz ] a
t23 = Xform id

t2All = t21 & t22 & t23
-- ghc gladly infers
-- t2All :: Xform '[Baz] '[Foo, Bar, Baz] a
-- indeed, this transformation has 'Baz' requirement unsatisfied due to 't22'

I'll see how well it integrates with the rest of pirouette tomorrow.

[VictorCMiraldo]

While I like this idea, we've decided against doing something like that a while ago for two reasons:

1. Lowers the complexity threshold for people to get into the codebase
2. Keeps pirouette as modular as possible: the engineer gets to pick which transformations should be applied, not the compiler.

That being said, and with pirouette becoming more and more domain specific (i.e., the PR about the execution semantics independent symbolic evaluation failing to deliver), I can see how it will help solidify the codebase and help catching refactoring mistakes.

Personally, I'm always all-in for some type-fu! :muscle:

[mmontin]

I like the fact that the type system helps us in applying the right transformations and I think that's relevant when transformation assume another one was previously done (for instance, assuming the terms will be in prenex form).

In terms of this attempt, it's very interesting, but I am wondering whether we can do better or not, because it seems to me that the type checker here does not enforce needed transformation to be called, but rather it gives in the type of the resulting transformation whether or not some additional constraints should be satisfied, that is when the first parameter of Xform is non-empty.

Could we somehow enforce it ?

To answer this question, I think we should look at :

• how Plutarch handles constraints in Value (namely NonZero and Positive)
• how optics uses Haskell's type system to handle the "subtyping" of optics depicted for instance in https://d1bv04v5uizu9x.cloudfront.net/assets/img/optics-downloadable/png/Optics%20downloadable_04.png

Is there anything we can learn from these to improve this solution?

[facundominguez]

Looks harmless enough if we are not storing transformations inside lists or collections where the type indices would make things tricky. @0xd34df00d made a good job at coming with a simple scheme.

But I'm still unconvinced that this is worth the trouble. When maintaining code I would expect to concern myself more with the reason of a dependency between transformations than with potentially missing a dependency when preparing a pipeline.

[0xd34df00d]

I'd be happy to drop this as well, so up to you folks as I'm obviously biased towards some type-level fun.

For the record, regarding @mmontin's question, the idea is that the type of the function that runs the pipeline is explicitly monomorphic, along the lines of

xform :: Xform '[] provides a -> a -> a
xform (Xform f) = f

Then, if you try to run something that has unsatisfied dependencies, GHC will complain along the lines of:

    • Couldn't match type: '[Prenex]
                     with: '[]