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

[Miguel Mitrofanov]

  So... you want your "ones" not to typecheck? Guess that's impossible, since it's nothing but "fix" application...

13.10.2010 12:33, 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
>>
>
>