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

[Jonas Almström Duregård]

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 at 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 at 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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20101013/f30ffb30/attachment.html