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

So all you need is a program that checks if your functions terminate. How hard can it be, right? ;) Seriously though, since you would need static termination guarantees on all functions that produce lists, you will be severely restricted when working with them. It's like Haskell without general recursion... Anyway, here's a quick version where you can do cons, map and ++. The idea is that any function that results in a larger list also results in a larger type. Any function that works on finite lists of type a can have type "Finite s a" as a parameter and since the finite module only exports the limited : and ++ functions it should be safe. The inferred type of "safeLength = length . infinite" is "safeLength :: Finite s a -> Int" for instance. {-# Language EmptyDataDecls #-} module Finite ( emp , (-:) , map , (++) , infinite , module Prelude ) where import Prelude hiding ((++), map) import qualified Prelude data Z data S a data Plus a b newtype Finite s a = Finite {infinite :: [a]} deriving Show instance Functor (Finite n) where fmap f = Finite . fmap f . infinite emp :: Finite Z a emp = Finite [] (-:) :: a -> Finite n a -> Finite (S n) a (-:) a l = Finite $ a : (infinite l) infixr 5 -: (++) :: Finite s1 a -> Finite s2 a -> Finite (S (Plus s1 s2)) a (++) (Finite a) (Finite b) = Finite $ a Prelude.++ b infixr 5 ++ map = fmap /J 2010/10/13 Eugene Kirpichov :

Well, it's easy to make it so that lists are either finite or bottom, but it's not so easy to make infinite lists fail to typecheck... That's what I'm wondering about.

2010/10/13 Miguel Mitrofanov :

...

hdList :: List a n -> Maybe a hdList Nil = Nothing hdList (Cons a _) = Just a

hd :: FiniteList a -> Maybe a hd (FL as) = hdList as

*Finite> hd ones

this hangs, so, my guess is that ones = _|_

13.10.2010 12:13, Eugene Kirpichov пишет:

...

{-# 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

_______________________________________________ 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/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe