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 <ekirpichov@gmail.com>:
> 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 <miguelimo38@yandex.ru>:
>> š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
>