How can I recursively define a sequence of types in Haskell?

Question

Specifically what I want to do is define, for each positive integer n, a type for lists of level n. By that I mean something that would look a bit like this (but maybe not exactly). First, for any type a let List a be [a]. (This I know how to do.) Now I would like

IteratedList 0 a = a

IteratedList n a = List (IteratedList (n-1) a)

So, for example, IteratedList 3 a would be [[[a]]].

The reason I want this is that I want to write a parser that can pick out a list of level n by recognising the opening bracket, picking out a bunch of lists of level n-1, and then recognising the closing bracket. But I don't know how to make the appropriate type declaration for the parser.

Maybe I'm going about things the wrong way. If so, then what is the right way?

Added later. Many thanks for the helpful answers below. In the end, prompted by (i) the difficulty of using anything like a nested-list concept and (ii) the comment by n.m. that suggested that I almost certainly didn't need to use one (as I half suspected), I realized that I could achieve what I wanted with my parser in a simple way that indeed did not require a type for nested lists. Useful lesson learnt.

Answer 1

I don't know what you want to do with your parsed representation of lists, so it's hard to give a "general enough" answer for this, so I'll make up a list and parse it, and you can tell me if it's what you're looking for.

import Data.List.Split
import Data.List(span)

data NestedList a = NestedList{ nesting :: Int, elems :: [a] } 
  deriving (Show, Eq)

testlist = "[ [ [1,2], [3,4], [5,6], [1] ], [ [9] ] ]"

parseList :: Read a => String -> NestedList [a]
parseList = merge . go 0
    where go n []       = []
          go n (x:xs) = case x of
            '[' -> go (n + 1) xs
            ']' -> go (n - 1) xs
            ',' -> go n xs
            ' ' -> go n xs
            _   ->  NestedList n (map read $ splitOn "," elems) : go n rest
                      where (elems, rest) = span (`notElem` "[]") (x:xs)
          merge [] = NestedList 0 []
          merge (NestedList n xs:ns) = 
            let next = elems (merge ns)
            in NestedList n (xs:next)

This is by no means perfect, particularly because that triple-nested 9 gets interpreted as "just another element," but it's a start.

*> parseList testlist :: NestedList [Int]
*> NestedList {nesting = 3, elems = [[1,2],[3,4],[5,6],[1],[9]]}

The idea is basically to keep track of how deep we're going when parsing the tree, build up a bunch of nested lists in the process, and then conglomerate them into one big nested list. Again, this isn't perfect, but it's a start (and a different approach than trying to shove dependent typing into Haskell ;) )

Answer 2

This is tricky, but do-able with some type level hacking. Sadly it's more complicated than you'd like.

I avoid closed type families so this will compile with GHC 7.6 and up

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Proxy

data Nat = S Nat | Z -- Type level natural numbers, Z means zero, S n means n + 1
type family IteratedList (n :: Nat) a
type instance IteratedList Z a     = [a]                -- Base case
type instance IteratedList (S n) a = [IteratedList n a] -- Inductive step

Notice that this works exactly like mathematical induction? We "prove" what IteratedList is when n is Z and then we can "prove" what it is when n is S n using IteratedList n a.

This actually can be taken to quite a deep level and we quickly start to bump against the bounds of poor GHC's open type families and end up needing GHC 7.8.

In order to help GHC's type checker with all of this, we need to provide what are called Proxys. These are just simple data types with a phantom type variable that we use to represent useful things for the type checker.

Here's a helper function we use later on which takes in a Proxy holding a number greater than zero, and returns a proxy with the number decremented by one.

predProxy :: Proxy (S n) -> Proxy n
predProxy = reproxy

Now we use type classes to generalize operations across IteratedLists. These classes essentially work like by induction. For example, here's the class to make a single element inside an IteratedList.

class Single (n :: Nat) a where
  single :: Proxy n -> a -> IteratedList n a
instance Single Z a where
  single _ = (:[])
instance Single n a => Single (S n) a where
  single p a = [single (predProxy p) a]

The Proxy n parameter is needed to help GHC's type checker understand what's going on, since otherwise it will generate a lot of fresh type variables and then stubbornly not unify them. Presumably there's a clever reason for this.

Notice that the two instances of the type class look really similar to how we defined IteratedList? one for Z, then an inductive step.

As far as constructing this at run time.. technically this is all just based on type synonyms, so you don't actually need a conversion routine, just to build the list. The tricky bit is that you either need to box that n in an existential or CPS your code so that you can have 1 return type.

Otherwise your return type would depend on your input and you can't express something so sophisticated to GHC.

You can imagine something like

buildIteratedList :: String -> (forall n. IteratedList n a -> r) -> r

but this quickly becomes quite horrid to work with since every operation needs to be a type class-induction-goop in order to be universal over n.

I'd suggest just doing something simple like

data Nested a = Elem a
              | List [Nested a]

and doing runtime checks.. Without dependent types this seems quite infeasible to me.

Answer 3

I wouldn't exactly recommend this, but you can use the new type level literal Nat machinery in GHC 7.8 to achieve this.

{-# LANGUAGE KindSignatures, TypeFamilies #-}

import GHC.TypeLits

type family IteratedList (n :: Nat) a where
    IteratedList 0 a = [a]
    IteratedList n a = IteratedList (n - 1) [a]

This makes use of a closed type family to recurse over the structure of Nat, adding type level layers of [] each time it recurses.