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