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