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
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Eugene Kirpichov Senior Software Engineer, Grid Dynamics http://www.griddynamics.com/