Inductive definition over closed type family

Question

This is more or the less the functionality I want to implement:

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE InstanceSigs           #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType             #-}

type family ReturnType arr where
  ReturnType (a -> b) = ReturnType b
  ReturnType a = a

type family ReplaceReturnType t r where
  ReplaceReturnType (a -> b) r = a -> ReplaceReturnType b r
  ReplaceReturnType _ r = r

class CollectArgs f where
  collectArgs :: ((forall r. ReplaceReturnType f r -> r) -> ReturnType f) -> f

instance CollectArgs f => CollectArgs (a -> f) where
  collectArgs :: ((forall r. (a -> ReplaceReturnType f r) -> r) -> ReturnType f) -> a -> f
  collectArgs f a = collectArgs (\ap -> f (\k -> ap (k a)))

instance (ReturnType a ~ a, ReplaceReturnType a dummy ~ dummy) => CollectArgs a where
  collectArgs :: ((forall r. ReplaceReturnType a r -> r) -> a) -> a
  collectArgs f = f id

What I eventually want to do with this is to write functions which are polymorphic in the number of incoming arguments, while they don't have to be part of a type class definition (which would correspond to printf var args style). So, for example:

wrapsVariadicFunction :: (CollectArgs f) => f -> Int -> f
wrapsVariadicFunction f config = collectArgs $ \apply -> 
  if odd config 
    then error "odd config... are you nuts?!"
    else apply f

Only that the return type of f might not coicide with that of wrapsVariadicFunction.

Now, in a perfect world where I can associate a type class with a closed type family (a closed type class, so to speak), this would be easy to implement, because the connection ReplaceReturnType a r ~ r would be clear.

Since I can't state that connection, it is, quite understandably, not clear to GHC 8.2.1:

    * Could not deduce: ReplaceReturnType a r ~ r
      from the context: (ReturnType a ~ a,
                         ReplaceReturnType a dummy ~ dummy)
        bound by the instance declaration
      `r' is a rigid type variable bound by
        a type expected by the context:
          forall r. ReplaceReturnType a r -> r
      Expected type: ReplaceReturnType a r -> r
        Actual type: r -> r
    * In the first argument of `f', namely `id'
      In the expression: f id
      In an equation for `collectArgs': collectArgs f = f id
    * Relevant bindings include
        f :: (forall r. ReplaceReturnType a r -> r) -> a
        collectArgs :: ((forall r. ReplaceReturnType a r -> r) -> a) -> a
   |
29 |   collectArgs f = f id
   |

A solution here would be universally quantifying over dummy in the instance context, but that's not possible (yet, judging from what I saw at ICFP). Also it's really cumbersome.

So, the actual question here is: How do I associate a value-level definition with a closed type family, much like a closed type class? Or is this impossible because types cannot be erased anymore? If so, is there some other workaround?

gallais gallais · Accepted Answer · 2017-09-14T11:17:06

The standard trick to have these type classes that look like they are overlapping is to add a second parameter to the typeclass which will be distinct in each instance and whose value can be computed from the other ones.

The idea distilled to its very core is as follows (we need some scary extensions like UndecidableInstances but that's fine: we're writing total programs):

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE UndecidableInstances   #-}

type family IsBase arr :: Bool where
  IsBase (a -> b) = 'False
  IsBase a        = 'True

class SillyId a b where
  sillyId :: IsBase a ~ b => a -> a

instance SillyId b (IsBase b) => SillyId (a -> b) 'False where
  sillyId f = \x -> sillyId (f x)

instance SillyId b 'True where
  sillyId t = t

Now, in your case it's a bit more complicated because you not only want this extra argument to do the dispatch, you also want other type level functions to reduce based on it. The trick is simply... to define these functions in terms of that dispatch!

Of course a type level Bool won't do anymore: you'll need to keep all of the information around. So instead of IsBase you'll have IsArrow:

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE InstanceSigs           #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE UndecidableInstances   #-}

type family IsArrow arr :: Either (*, *) * where
  IsArrow (a -> b) = 'Left '(a, b)
  IsArrow a        = 'Right a

type family ReturnType arr where
  ReturnType ('Left '(a, b)) = ReturnType (IsArrow b)
  ReturnType ('Right a)      = a

type family ReplaceReturnType t r where
  ReplaceReturnType ('Left '(a, b)) r = a -> ReplaceReturnType (IsArrow b) r
  ReplaceReturnType _               r = r

class CollectArgs f (f' :: Either (*, *) *) where
  collectArgs :: IsArrow f ~ f' => ((forall r. ReplaceReturnType f' r -> r) -> ReturnType f') -> f

instance CollectArgs f (IsArrow f) => CollectArgs (a -> f) ('Left '(a, f)) where
  collectArgs :: ((forall r. (a -> ReplaceReturnType (IsArrow f) r) -> r) -> ReturnType (IsArrow f)) -> a -> f
  collectArgs g a = collectArgs (\ap -> g (\k -> ap (k a)))

instance CollectArgs a ('Right a) where
  collectArgs :: IsArrow a ~ 'Right a => ((forall r. ReplaceReturnType (IsArrow a) r -> r) -> a) -> a
  collectArgs f = f id

And voilà. You can of course define type synonyms for ReplaceReturnType (IsArrow a) r to make the notations a bit lighter but that's the gist of it.

Inductive definition over closed type family

1 Answers