Closed type families and strange function types

8
votes

Sorry, I couldn't imagine any better title for the question, so please read ahead. Imagine that we have a closed type family that maps every type to it's corresponding Maybe except maybes themselves:

type family Family x where
  Family (Maybe x) = Maybe x
  Family x = Maybe x

We can even declare a function using that type family:

doMagic :: a -> Family a
doMagic = undefined

exampleA = doMagic $ Just ()
exampleB = doMagic $ ()

Playing with it in GHCi shows that it is ok to evaluate the type of this function application:

*Strange> :t exampleA      
exampleA :: Maybe ()       
*Strange> :t exampleB      
exampleB :: Maybe ()

The question is if it is possible to provide any implementation of the doMagic function except undefined? Let's for example say that I would like to wrap every value into a Just constructor, except Maybes which should remain intact, how could I do that? I tried using typeclasses, but failed to write a compileable signature for doMagic function if not using closed type families, could somebody please help me?

2
haskelltype-families
In a dynamically typed language doMagic x = Just undefined would also respect types. Theoretically speaking, a type system could allow this (but would that be really useful?). BTW, the example you describe, if which you do different things depending of which concrete type a is, would require type information at runtime, while Haskell was designed to allow type erasure (no type info at runtime). You could get something close using a type class, though. – chi
Further, the question looks related to "what is the free theorem of a type in the presence of closed type families?". – chi

2 Answers

8
votes

You can use another closed type family to distinguish Maybe x from x and then you can use another typeclass to provide separate implementations of doMagic for these two cases. Quick and dirty version:

{-# LANGUAGE TypeFamilies, MultiParamTypeClasses,
    FlexibleInstances, UndecidableInstances, ScopedTypeVariables #-}

type family Family x where
  Family (Maybe x) = Maybe x
  Family x = Maybe x

data True
data False

type family IsMaybe x where
  IsMaybe (Maybe x) = True
  IsMaybe x = False


class DoMagic a where
  doMagic :: a -> Family a

instance (DoMagic' (IsMaybe a) a (Family a)) => DoMagic a where
  doMagic = doMagic' (undefined :: IsMaybe a)   


class DoMagic' i a r where
  doMagic' :: i -> a -> r

instance DoMagic' True (Maybe a) (Maybe a) where
  doMagic' _ = id

instance DoMagic' False a (Maybe a) where
  doMagic' _ = Just


exampleA = doMagic $ Just ()
exampleB = doMagic $ ()
4
votes

You can sort of make a doMagic function that hobbles along. Unfortunately, closed-ness of the type family doesn't really help you much. Here's how a start might look

{-# LANGUAGE TypeFamilies #-}

type family Family x where
    Family (Maybe x) = Maybe x
    Family x = Maybe x

class Magical a where doMagic :: a -> Family a
instance Magical (Maybe a) where doMagic = id
instance Magical () where doMagic = Just

You can see it working in ghci just as you asked:

*Main> doMagic $ Just ()
Just ()
*Main> doMagic $ ()
Just ()

So why do I say it's hobbling along? Well, you may have noticed that the two provided instances don't cover very much of the Haskell ecosystem of types:

*Main> doMagic $ True
<interactive>:3:1:
    No instance for (Magical Bool) arising from a use of ‘doMagic’
    In the expression: doMagic
    In the expression: doMagic $ True
    In an equation for ‘it’: it = doMagic $ True

So one would have to provide instances for every type (constructor) of interest. Indeed, not even incoherent instances -- the club with which many such problems can be beat into submission -- helps here; if one tries to write

instance Magical (Maybe a) where doMagic = id
instance Magical a where doMagic = Just

the compiler rightly complains that after all we don't know that the fully polymorphic instance actually has the right type. The thing about incoherent instances is that we aren't told by the compiler that, just because that was the instance chosen, that the other instances definitely don't apply. So it's possible that we choose the fully polymorphic instance at some point, only to later discover that we were really a Maybe behind the scenes, and then we just wrapped one too many layers of Maybe around things. Unfortunate.

There is not much that can be done about this at the moment. Closed type families at the moment just do not provide all the knowledge one might wish to have available. Perhaps some day GHC will offer a mechanism that makes closed type families more useful in this regard such as a type inequality constraint, but I wouldn't hold my breath: it is a research problem how to provide this useful information, and I haven't heard any rumors of people tackling it.