CODEWITHSUNDEEP
haskelltypes
lukerandall
lukerandall

Reputation: 2212

Write length function for list with statically typed length

Given a list with a statically typed length (taking this as an example):

data Zero

data Succ nat

data List el len where
    Nil  ::                      List el Zero
    Cons :: el -> List el len -> List el (Succ len)

is it possible to write a length function that calculates the length using the static typing rather than the usual recursion?

My efforts thus far have led me to the conclusion that it is not possible, as it would require "unlifting" the type information in order to recur on it:

class HasLength a where
    length :: a -> Natural

instance HasLength (List el Zero) where
    length _ = 0

instance HasLength (List el (Succ len)) where
    length _ = 1 + *how to recur on type of len*

However, I am only just beginning to learn about all the magic possible with types, so I know that my not being able to conceive of a solution does not imply the absence of one.

update

Since length returns Natural, I incorrectly wrote length _ = 1 + .... The correct instance (using the answer given below) is

instance HasLength (List el len) => HasLength (List el (Succ len)) where
    length _ = succ $ length (undefined :: List el len)

Upvotes: 5

Views: 182

Answers (2)

applicative
applicative

Reputation: 8199

This will be much easier if you use the DataKinds extension, which will allow you to 'promote' Natural to a kind, which makes the (promoted) types Zero and Succ n more tractable and eliminates nonsense like Succ Char. There are several ways of going about it, but sticking close to your text:

{-#LANGUAGE GADTs, DataKinds, StandaloneDeriving  #-}
data Natural = Zero | Succ Natural deriving (Show,Eq,Ord)

data List el len  where
    Nil  ::                      List el Zero 
    Cons :: el -> List el len -> List el (Succ len) 

deriving instance Show el => Show (List el len)

class HasLength f where len ::  f n -> Natural

instance HasLength (List el) where
    len Nil = Zero
    len (Cons _ xs) = Succ (len xs)

(I also used StandaloneDeriving, which is needed to automatically derive Show in such cases.)

Upvotes: 1

Ed'ka
Ed'ka

Reputation: 7140

For example like this:

instance HasLength (List el len) => HasLength (List el (Succ len)) where
    length _ = 1 + length (undefined :: List el len)

Note: this requires ScopedTypeVariables extension.

Upvotes: 8

Related Questions