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

[Steffen Schuldenzucker]

I don't know too much about GADTs, but it works fine with fundeps:

http://hpaste.org/40535/finite_list_with_fundeps

(This is rather a draft. If anyone can help me out with the TODOs, I'd be happy.)

-- Steffen


On 10/13/2010 10:40 AM, Eugene Kirpichov wrote:
> Well, in my implementation it's indeed impossible. It might be
> possible in another one. That is the question :)
> Perhaps we'll have to change the type of cons, or something.
> 
> 13 октября 2010 г. 12:37 пользователь Miguel Mitrofanov
> <miguelimo38 at yandex.ru> написал:
>>  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
>>>>
>>>
>>>
>>
> 
> 
>