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

[Steffen Schuldenzucker]

Hmm, ok, I simplified the idea[1] and it looks like I'm getting the same
problem as you when trying to drop the 'n' parameter carrying the length of
the list.

Sad thing.

[1] http://hpaste.org/40538/finite_list__not_as_easy_as_i

On 10/13/2010 10:43 AM, Steffen Schuldenzucker wrote:
> 
> 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
>>>>>
>>>>
>>>>
>>>
>>
>>
>>
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe