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?
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):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 ofIsBase
you'll haveIsArrow
: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.