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

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 написал:

...

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:

...

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