CODEWITHSUNDEEP
listhaskellinfinite
flawr
flawr

Reputation: 11628

finite recursive "List" type

It is easy to reconstruct the list type in Haskell:

data MyList a = Cons a (MyList a)
               | Empty
               deriving (Show)

someList = Cons 1 (Cons 2 (Cons 3 Empty)) -- represents [1,2,3]

This allows for constructing infinites lists. Is it possible to somehow define a list type, that only allows for finite (but still arbitrary length) lists?

The example of lists here can replaced with any other potentially infinite data structures like trees etc. Note that I do not have any particular application in mind, so there is no need to question the usefullness of this, I'm just curious whether that would be possible.

Upvotes: 5

Views: 796

Answers (1)

chi
chi

Reputation: 116139

Alternative 1: lists with a strict tail

data MyList a = Cons a !(MyList a) | Empty

Trying to build an infinite list will surely lead to a bottom element of MyList a.

Alternative 2: existentially-quantified fixed-length list

data Nat = O | S Nat
data List a (n :: Nat) where
   Nil :: List a O
   Cons :: a -> List a n -> List a (S n)
data MyList a where
   MyList :: List a n -> MyList a

I would say that this does not allow for infinite lists as well.

This is because we can't pattern match on a GADT with where (or lazy patterns in general).

-- fails to compile
test :: MyList Int
test = MyList (Cons 1 list)
       where MyList list = test

The following would be too strict.

-- diverges
test2 :: MyList Int
test2 = case test2 of
          MyList list -> MyList (Cons 1 list)

The following makes the existentially quantified type variable "escape" the scope of the case:

-- fails to compile
test3 :: MyList Int
test3 = MyList $ case test3 of
          MyList list -> (Cons 1 list)

Upvotes: 6

Related Questions