Last post, I explained when you could use rankNTypes. I've been using them for a while, and am reasonably happy with them. I still consider them an experimental feature, and there are things I don't like about them.

We start by building on the previous blog post, this will present us with a 'user view' of rankNTypes:

{-# OPTIONS_GHC -Wall #-} -- show almost all warnings
{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}
module TestDAGS where
import MyDAGS
import Data.Coerce
import Control.Monad.Identity

someDAG1 :: forall name. WithDAGT name (RefN name)
someDAG1 = do dagnode1 <- addNode "node1" []
              dagnode2 <- addNode "node2" [dagnode1]
              return dagnode2

Even the type deriving works as intended: the above type was derived automatically by GHC (and then copied from the warning). Ideally, all the difficult stuff is written in the MyDAGS library, and users only need some basic Haskell. So let's see where this goes wrong.

Using showDAG

An obvious thing a user might do, is execute runDAG on someDAG1. This should not be allowed: if we want to get a reference out of the monad (through runDAG), we get an error:

*TestDAGS> let run = runDAG someDAG1

<interactive>:1:18:
    Couldn't match type 'a0' with 'RefN name'
      because type variable 'name' would escape its scope (..)

Now this is desired behavior! Now what about showDAG? It does not do anything with the return value, so that should work right?

*TestDAGS> :t showDAG
showDAG :: (forall name. WithDAGT name a) -> String
*TestDAGS> showDAG someDAG1

<interactive>:3:9:
    Couldn't match type 'a0' with 'RefN name'
      because type variable 'name' would escape its scope (..)

Here I am only slightly disappointed: we can still fix this:

showDAG1 :: String
showDAG1 = showDAG (do _dagnode2 <- someDAG1
                       return ())

Success! Again, all the types were derived automatically. It would be nice if we can give someDAG1 as an argument to a version of showDAG. The type-checker will not derive a type for the next bit of code. That is inconvenient, but the most generic type here would be that of showDAG anyways, which is what we wish to avoid here.

This works:

showDAG2 :: forall m. (forall name. WithDAGT name (m name)) -> String
showDAG2 sdag = showDAG (do _dagnode2 <- sdag
                            return ())
*TestDAGS> showDAG2 someDAG1
"DAG [Node \"node1\" [],Node \"node2\" [RefN 0]]"

Great, now to the next DAG:

someDAG2 :: forall name. WithDAGT name [RefN name]
someDAG2 = do dagnode1 <- addNode "node1" []
              dagnode2 <- addNode "node2" [dagnode1]
              return [dagnode1,dagnode2]

We will need yet another version of showDAG: showDAG2 someDAG1 will not work. We might be writing quite a few versions of showDAG, all with the same code as showDAG2.

Lists of DAGs

Next, we will try to do something with a list of DAGs:

someDAGS1 :: forall name. [WithDAGT name (RefN name)]
someDAGS1 = [someDAG1,someDAG1]

Again the type derivation is automatic. We can map things across a list, so let's get rid of those pesky RefNs that have bothered us previously:

hideRef :: forall t m. Monad m => m t -> m ()
hideRef dag = do _node <- dag
                 return ()
someDAGS2 :: forall name. [WithDAGT name ()]
someDAGS2 = map hideRef someDAGS1

All types here are derived automatically, GHC works like a charm so far. Now for something more complicated:

*TestDAGS> map showDAG someDAGS2

<interactive>:12:5:
    Couldn't match type 'WithDAGT name0 ()'
                   with 'forall name. WithDAGT name a0'

If we wish to map showDAG, we would have to apply it with something of the type [forall name. WithDAGT name a], such that a does not contain name. That requires ImpredicativeTypes. If it would solve the problem, that would be okay. Unfortunately, the following attempt fails, and not just because of type role WithDAGT nominal nominal (it also does not work without that):

 test :: (forall name. [WithDAGT name ()]) -> [forall name. WithDAGT name ()]
 test dags = coerce dags

So, we are forced to iterate over the list to do, essentially, nothing. This is not as trivial as it seems, but let me start on what does work:

test2 :: (forall name. [WithDAGT name ()]) -> [forall name. WithDAGT name ()]
test2 [] = []
test2 x = hRes ++ test2 tl
  where (h:tl) = x
        hRes :: [forall name. WithDAGT name ()]
        hRes = [h]

Now I'll go through several alternatives that do not work:

 test3 :: (forall name. [WithDAGT name ()]) -> [forall name. WithDAGT name ()
 test3 [] = []
 test3 (h:tl) = hRes ++ test3 t
    where hRes :: [forall name. WithDAGT name ()]
          hRes = [h]

The reason the above does not work, is that generalization does not happen at the left hand side of an assignment. An equivalent structure with case won't work either. Removing the ++ and [] on hRes is something I would very much like to do, but these do not work:

 test4a :: (forall name. [WithDAGT name ()]) -> [forall name. WithDAGT name ()]
 test4a [] = []
 test4a x = hRes : test4a tl
   where (h:tl) = x
         hRes :: (forall name. WithDAGT name ())
         hRes = h

 test4b :: (forall name. [WithDAGT name ()]) -> [forall name. WithDAGT name ()]
 test4b [] = []
 test4b x = runIdentity hRes : test4b tl
   where (h:tl) = x
         hRes :: Identity (forall name. WithDAGT name ())
         hRes = Identity h

In the case of test4a, the forall name. seems to be optimized away too soon by the type-checker. It complains that hRes has the type WithDAGT name0 (), where, (forall name. WithDAGT name ()) is literally the desired type. For test4b, I'm in the dark on why this does not work. GHC complains about the last line, and it does so with every user defined type I could think of. Built-in types, on the other hand, seem to be fine:

test5 :: (forall name. [WithDAGT name ()]) -> [forall name. WithDAGT name ()]
test5 [] = []
test5 x = fst hRes : test5 (tail x)
  where hRes :: (forall name. WithDAGT name (), Int)
        hRes = (head x,3)

The above works again. In practice, I found it very hard to predict when the type checker would find my programs correct, and when not.

Data.Coerce

The solution to some of the problems, is to use "Data.Coerce" to get zero-cost type conversions. Unfortunately, the role declarations like type role RefN nominal are limiting the possibilities. This section is to convince you that removing such lines are not an option.

I imported "Data.Coerce" to do get some undesired behavior, which only works if the line type role RefN nominal is omitted in MyDAGS. I do not believe this is a real problem: I can live with writing that line. Whether or not I should write it or not, is just a matter of choosing which is the default. Apparently, my use of RankNTypes is not the most common use for phantom types.

 someNode :: forall name name2. WithDAGT name2 (RefN name)
 someNode = do dagnode1 <- addNode "nodeX" []
               return (coerce dagnode1)
 freeNode :: forall name. (RefN name)
 freeNode = fst (runDAG someNode)

So, if you read my previous post, you'll see why this is bad: we were only supposed to be able to get nodes of the type RefN (), such that we could not re-use them. This is exactly what I'll do to create a 'wrong' DAG:

 someDAG2 :: forall name. WithDAGT name ()
 someDAG2 = do _dagnode  <- addNode "node1" [freeNode]
               return ()

Then in GHCI:

*TestDAGS> putStrLn (showDAG someDAG2)
DAG [Node "node1" [RefN 0]]

This shows the first node pointing to itself (and not to nodeX, which is not inside this DAG). Note that even with the line type role RefN nominal, we are able to write someNode inside MyDAGS.lhs because RefN is exposed there. That behavior is fine with me too: if it is done within MyDAGS.lhs, the person doing it should be careful anyway.