[Haskell-cafe] Finite but not fixed length...

[Eugene Kirpichov]

Hm. This is not actually an answer to your question, just a
"discussion starter", but still.

The code below typechecks, though actually it shouldn't: there's no
type "n" such that "ones" is formed by the FL from some value of type
List Int n.
Or should it?

{-# LANGUAGE ExistentialQuantification, GADTs, EmptyDataDecls #-}
module Finite where

data Zero
data Succ a

class Finite a where

instance Finite Zero
instance (Finite a) => Finite (Succ a)

data List a n where
  Nil :: List a Zero
  Cons :: (Finite n) => a -> List a n -> List a (Succ n)

data FiniteList a where
  FL :: (Finite n) => List a n -> FiniteList a

nil :: FiniteList a
nil = FL Nil

cons :: a -> FiniteList a -> FiniteList a
cons a (FL x) = FL (Cons a x)

list123 = cons 1 (cons 2 (cons 3 nil))

ones = cons 1 ones -- typechecks ok

2010/10/13 Jason Dusek <jason.dusek at gmail.com>:
>  Is there a way to write a Haskell data structure that is
>  necessarily only one or two or seventeen items long; but
>  that is nonetheless statically guaranteed to be of finite
>  length?
>
> --
> Jason Dusek
> Linux User #510144 | http://counter.li.org/
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



-- 
Eugene Kirpichov
Senior Software Engineer,
Grid Dynamics http://www.griddynamics.com/