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 >> <miguelim...@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<miguelim...@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@haskell.org >>>>> http://www.haskell.org/mailman/listinfo/haskell-cafe >>>>> >>>> >>>> >>> >> >> >> > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe