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

[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 <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/