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...<br>
<br>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.<div>
<br><font class="Apple-style-span" face="'courier new', monospace">{-# Language EmptyDataDecls #-}<br><br>module Finite (<br> š šemp<br> š, (-:)<br> š, map<br> š, (++)<br> š, infinite<br> š, module Prelude<br> š) where<br>
<br>import Prelude hiding ((++), map)<br>import qualified Prelude<br><br>data Z<br>data S a<br>data Plus a b<br><br>newtype Finite s a = Finite {infinite :: [a]} deriving Show<br><br>instance Functor (Finite n) where<br> šfmap f = Finite . fmap f . infinite<br>
<br>emp :: Finite Z a<br>emp = Finite []<br><br>(-:) :: a -> Finite n a -> Finite (S n) a <br>(-:) a l = Finite $ a š: (infinite l)<br>infixr 5 -:<br><br>(++) :: Finite s1 a -> Finite s2 a -> Finite (S (Plus s1 s2)) a<br>
(++) (Finite a) (Finite b) = Finite $ a Prelude.++ b<br>infixr 5 ++<br><br>map = fmap</font><br><br><br>/J<br><br>2010/10/13 Eugene Kirpichov <<a href="mailto:ekirpichov@gmail.com">ekirpichov@gmail.com</a>>:<br>> Well, it's easy to make it so that lists are either finite or bottom,<br>
> but it's not so easy to make infinite lists fail to typecheck...<br>> That's what I'm wondering about.<br>><br>> 2010/10/13 Miguel Mitrofanov <<a href="mailto:miguelimo38@yandex.ru">miguelimo38@yandex.ru</a>>:<br>
>> šhdList :: List a n -> Maybe a<br>>> hdList Nil = Nothing<br>>> hdList (Cons a _) = Just a<br>>><br>>> hd :: FiniteList a -> Maybe a<br>>> hd (FL as) = hdList as<br>>><br>
>> *Finite> hd ones<br>>><br>>> this hangs, so, my guess is that ones = _|_<br>>><br>>><br>>> 13.10.2010 12:13, Eugene Kirpichov ĐÉŰĹÔ:<br>>>><br>>>> {-# LANGUAGE ExistentialQuantification, GADTs, EmptyDataDecls #-}<br>
>>> module Finite where<br>>>><br>>>> data Zero<br>>>> data Succ a<br>>>><br>>>> class Finite a where<br>>>><br>>>> instance Finite Zero<br>>>> instance (Finite a) => šFinite (Succ a)<br>
>>><br>>>> data List a n where<br>>>> š Nil :: List a Zero<br>>>> š Cons :: (Finite n) => ša -> šList a n -> šList a (Succ n)<br>>>><br>>>> data FiniteList a where<br>
>>> š FL :: (Finite n) => šList a n -> šFiniteList a<br>>>><br>>>> nil :: FiniteList a<br>>>> nil = FL Nil<br>>>><br>>>> cons :: a -> šFiniteList a -> šFiniteList a<br>
>>> cons a (FL x) = FL (Cons a x)<br>>>><br>>>> list123 = cons 1 (cons 2 (cons 3 nil))<br>>>><br>>>> ones = cons 1 ones -- typechecks ok<br>>><br>>> _______________________________________________<br>
>> Haskell-Cafe mailing list<br>>> <a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>>> <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
>><br>><br>><br>><br>> --<br>> Eugene Kirpichov<br>> Senior Software Engineer,<br>> Grid Dynamics <a href="http://www.griddynamics.com/">http://www.griddynamics.com/</a><br>> _______________________________________________<br>
> Haskell-Cafe mailing list<br>> <a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>> <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
><br><br></div>