Bidirectional Type Family Inference

Problem

Imagine you have a relation, say, R x y z such that x and y uniquely determine z, and z uniquely determines x and y. You have to use the relation in a type signature in such a way that x and y can be inferred from z, and vice versa.

We'll use this relation as an example: R True e (e, e) R False e (e, e, e)

Attempt 1: Fundeps in MPTC

Let's try solving this with functional dependencies in multi-parameter typeclasses! {-# LANGUAGE DataKinds, MultiParamTypeClasses, FunctionalDependencies, KindSignatures, FlexibleInstances #-} class R (x :: Bool) y z | x y -> z, z -> x y where xy2z :: Proxy x -> y -> z; xy2z = undefined -- for demonstration purposes z2x :: z -> Proxy x; z2x = undefined z2y :: z -> y; z2y = undefined instance R True e (e, e) instance R False e (e, e, e)

Let's test this out!
xy2z (Proxy :: Proxy True) () has type ((), ()), nice!
xy2z (Proxy :: Proxy False) 3 has type Num t => (t, t, t), great, now let's test the reverse:
z2y ((), ()) has type ()
z2y (2, 7) has type... Could not deduce (R x0 y (t0, t2)) arising from the ambiguity check for ‘it’ from the context (R x y (t1, t3), Num t1, Num t3) bound by the inferred type for ‘it’: (R x y (t1, t3), Num t1, Num t3) => y The type variables ‘x0’, ‘t0’, ‘t2’ are ambiguous When checking that ‘it’ has the inferred type ‘forall (x :: Bool) y t1 t2. (R x y (t1, t2), Num t1, Num t2) => y’ Probable cause: the inferred type is ambiguous

No go. The typechecker can't infer a ~ b from R x y (a, b)

Attempt 2: Closed Type Families

What if we define R as a type family taking x and y and returning z? {-# LANGUAGE DataKinds, TypeFamilies, KindSignatures #-} type family R (x :: Bool) y where R True e = (e, e) R False e = (e, e, e) xy2z :: Proxy x -> y -> R x y; xy2z = undefined z2xy :: R x y -> (Proxy x, y); z2xy = undefined

xy2z (Proxy :: Proxy True) 3 has type Num t => (t, t), but if we try to typecheck z2xy ((), ())... Couldn't match expected type ‘((), ())’ with actual type ‘R x y’ The type variables ‘x’, ‘y’ are ambiguous

Even though it's obvious from the definition of R (and the fact that it's closed), the typechecker can't derive y ~ () from R x y ~ ((), ())

Attempt 3: Inverse Families

If z uniquely determines x and y, we can build two type families that turn z into x, and into y: {-# LANGUAGE DataKinds, TypeFamilies, KindSignatures #-} type family R (x :: Bool) y where R True e = (e, e) R False e = (e, e, e) type family ZToX z where ZToX (e, e') = True ZToX (e, e', e'') = False type family ZToY z where ZToY (e, e') = e ZToY (e, e', e'') = e xy2z :: Proxy x -> y -> R x y; xy2z = undefined z2xy :: z -> (Proxy (ZToX z), ZToY z); z2xy = undefined

Note that ZToX and ZToY accept types that, strictly speaking, cannot be outputs of R, this is a rather important point.

z2xy now works as expected, z2xy (4, 0) infers the type Num t => (Proxy True, t).

Is this it? No. xy2z can infer the type of the result from the types of arguments, but it can't infer the types of the arguments from the type of the result! Even though z2xy successfully accomplishes an equivalent task! We have a type family for inferring z from x and y, a type family for inferring x from z, and a type family for inferring y from z; why can't we make a type that can infer in both directions simultaneously?

We can. Just throw the three type families into one type signature in the only way that makes sense: xy2z :: (z ~ R x y, x ~ ZToX z, y ~ ZToY z) => Proxy x -> y -> z; xy2z = undefined z2xy :: (z ~ R x y, x ~ ZToX z, y ~ ZToY z) => z -> (Proxy x, y); z2xy = undefined

Now both xy2z and z2xy can infer the types of their arguments in all ways implied by the original relation. Bonus points: > z2xy (_, ()) Found hole ‘_’ with type: () That is, a ~ b is inferred from R x y (a, b).

The comments section is closed