Re: [Haskell-cafe] Finite but not fixed length...
2010/10/13 Jonas Almström Duregård : > ...and you can always do > > hack :: Vec n a -> FixedVec a > hack x :: FixedVec undefined > > Also I'm guessing 1, 2 and 17 are just examples, he really wants arbitrary > length finite lists. Indeed. Where I said "is necessarily" I meant "is not necessarily". -- Jason Dusek Linux User #510144 | http://counter.li.org/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Finite but not fixed length...
...and you can always do hack :: Vec n a -> FixedVec a hack x :: FixedVec undefined Also I'm guessing 1, 2 and 17 are just examples, he really wants arbitrary length finite lists. /J On 13 October 2010 20:47, Daniel Peebles wrote: > One option could be something like: > > data Z > data S n > > data Vec n a where > Nil :: Vec Z a > Cons :: a -> Vec n a -> Vec (S n) a > > data Length n where > One :: Length (S Z) > Two :: Length (S (S Z)) > Seventeen :: Length (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S > Z) > > data FixedVec a where > FixedVec :: Legnth n -> Vec n a -> FixedVec a > > But it's obviously rather cumbersome :) > > > On Wed, Oct 13, 2010 at 7:57 AM, Jason Dusek wrote: > >> Is there a way to write a Haskell data structure that is >> necessarily only one or two or seventeen items long; but >> that is nonetheless statically guaranteed to be of finite >> length? >> >> -- >> Jason Dusek >> Linux User #510144 | http://counter.li.org/ >> ___ >> 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
Re: [Haskell-cafe] Finite but not fixed length...
One option could be something like: data Z data S n data Vec n a where Nil :: Vec Z a Cons :: a -> Vec n a -> Vec (S n) a data Length n where One :: Length (S Z) Two :: Length (S (S Z)) Seventeen :: Length (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z) data FixedVec a where FixedVec :: Legnth n -> Vec n a -> FixedVec a But it's obviously rather cumbersome :) On Wed, Oct 13, 2010 at 7:57 AM, Jason Dusek wrote: > Is there a way to write a Haskell data structure that is > necessarily only one or two or seventeen items long; but > that is nonetheless statically guaranteed to be of finite > length? > > -- > Jason Dusek > Linux User #510144 | http://counter.li.org/ > ___ > 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
Re: [Haskell-cafe] Finite but not fixed length...
Thanks everyone for your thoughtful replies. I might have expected a referral to a paper; it's a pleasant surprise to have these worked examples. -- Jason Dusek Linux User #510144 | http://counter.li.org/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Finite but not fixed length...
Hi Jonas Thanks - I was anticipating a type like this for the destructor: viewl :: Finite s a -> Either () (a, Finite (Predecessor s) a) I didn't appreciate that the size type in your code represented the upper bound and not the actual size. Best wishes Stephen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Finite but not fixed length...
>Then viewl can be defined anywhere, > >viewl :: Finite s a -> Either () (a, Finite s a) >viewl = finite (Left ()) (Right . (,)) ... or more like: viewl :: Finite s a -> Either () (a, Finite s a) viewl = finite (Left ()) (\a b -> Right (a,b)) /J 2010/10/13 Jonas Almström Duregård > Hi Stephen, > > I'm not sure I see the problem. You can do what you require with the > function i supplied (minus the typo). This is in the module (where the > Finite constructor is exposed) > > finite :: b -> (a -> Finite s a -> b) -> Finite s a -> b > finite b _ (Finite []) = b > finite _ f (Finite (x:xs)) = f x (Finite xs) > > Then viewl can be defined anywhere, > > viewl :: Finite s a -> Either () (a, Finite s a) > viewl = finite (Left ()) (Right . (,)) > > Why would you ever decrease the Peano numbers? It's just an upper bound, > not an exact size. > > /J > > 2010/10/13 Stephen Tetley : > > > Hi Jonas > > > > Thanks - I was meaning an equivalent to viewl on Data.Sequence, on plain > lists: > > > > viewl :: [a] -> Either () (a,[a]) > > viewl [] = Left () > > viewl (x:xs) = Right (x,xs) > > > > > > It was a trick question because I can't see how you can do it without > > decrement on the Peano numbers. > > > > Best wishes > > > > Stephen > > > > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Finite but not fixed length...
Hi Stephen, I'm not sure I see the problem. You can do what you require with the function i supplied (minus the typo). This is in the module (where the Finite constructor is exposed) finite :: b -> (a -> Finite s a -> b) -> Finite s a -> b finite b _ (Finite []) = b finite _ f (Finite (x:xs)) = f x (Finite xs) Then viewl can be defined anywhere, viewl :: Finite s a -> Either () (a, Finite s a) viewl = finite (Left ()) (Right . (,)) Why would you ever decrease the Peano numbers? It's just an upper bound, not an exact size. /J 2010/10/13 Stephen Tetley : > Hi Jonas > > Thanks - I was meaning an equivalent to viewl on Data.Sequence, on plain lists: > > viewl :: [a] -> Either () (a,[a]) > viewl [] = Left () > viewl (x:xs) = Right (x,xs) > > > It was a trick question because I can't see how you can do it without > decrement on the Peano numbers. > > Best wishes > > Stephen > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Finite but not fixed length...
Hi Jonas Thanks - I was meaning an equivalent to viewl on Data.Sequence, on plain lists: viewl :: [a] -> Either () (a,[a]) viewl [] = Left () viewl (x:xs) = Right (x,xs) It was a trick question because I can't see how you can do it without decrement on the Peano numbers. Best wishes Stephen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Finite but not fixed length...
On Wed, Oct 13, 2010 at 12:13:29PM +0400, Eugene Kirpichov wrote:
> Hm. This is not actually an answer to your question, just a
> "discussion starter", but still.
>
> The code below typechecks, though actually it shouldn't: there's no
> type "n" such that "ones" is formed by the FL from some value of type
> List Int n.
> Or should it?
>
> {-# 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
Fascinating. Doing
ones' = Cons 1 ones'
of course does not typecheck (as expected) with an occurs check error
(can't unify n = S n). But
ones = cons 1 ones
does typecheck. And it makes sense: I can see why cons has the type
it does, and given that type for cons this definition of ones is
perfectly well-typed. But the upshot, which I had never considered,
seems to be that existentially quantified types are allowed to be _|_.
-Brent
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Finite but not fixed length...
>Why do you have the S in the return type of Finite.++ ? Typo. Plus is sufficient. What I would really like is a nice way of implementing concat (i.e. concatenate a finite number of finite lists, of various "sizes", into a single finite list). /J 2010/10/13 Ozgur Akgun > Jonas, > > 2010/10/13 Jonas Almström Duregård > > (++) :: Finite s1 a -> Finite s2 a -> Finite (S (Plus s1 s2)) a >> (++) (Finite a) (Finite b) = Finite $ a Prelude.++ b >> infixr 5 ++ > > > Why do you have the S in the return type of Finite.++ ? > > Ozgur > > ___ > 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
Re: [Haskell-cafe] Finite but not fixed length...
Jonas, 2010/10/13 Jonas Almström Duregård > (++) :: Finite s1 a -> Finite s2 a -> Finite (S (Plus s1 s2)) a > (++) (Finite a) (Finite b) = Finite $ a Prelude.++ b > infixr 5 ++ Why do you have the S in the return type of Finite.++ ? Ozgur ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Finite but not fixed length...
> Nice, but how about a list destructor I'm not sure what you mean by destructor, if you mean an eliminator for case analysis then you can make a function finite :: b -> (a -> Finite s1 a -> b) -> Finite s2 a -> b finite b _ (Finite []) = b finite _ f (Finite (x:xs)) = f x xs If you men functions that possibly remove elements from lists, then you can add definitions like these to the module: filter = onList . Prelude.filter tail = onList Prelude.tail onList :: ([a] -> [b]) -> Finite s a -> Finite s b onList f = Finite . f . infinite Don't export onList though! filter and map should be enough to define any list function you want outside the module. Note that the size-type doesn't correspond exactly to the size of the list, but that's not really a problem as long as you only want to guarantee finiteness. /J On 13 October 2010 16:41, Stephen Tetley wrote: > Hi Jonas > > Nice, but how about a list destructor? > > ;-) > ___ > 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
Re: [Haskell-cafe] Finite but not fixed length...
Hi Jonas Nice, but how about a list destructor? ;-) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Finite but not fixed length...
So all you need is a program that checks if your functions terminate. How
hard can it be, right? ;) Seriously though, since you would need static
termination guarantees on all functions that produce lists, you will
be severely restricted when working with them. It's like Haskell without
general recursion...
Anyway, here's a quick version where you can do cons, map and ++. The idea
is that any function that results in a larger list also results in a larger
type. Any function that works on finite lists of type a can have type
"Finite s a" as a parameter and since the finite module only exports the
limited : and ++ functions it should be safe. The inferred type of
"safeLength = length . infinite" is "safeLength :: Finite s a -> Int" for
instance.
{-# Language EmptyDataDecls #-}
module Finite (
emp
, (-:)
, map
, (++)
, infinite
, module Prelude
) where
import Prelude hiding ((++), map)
import qualified Prelude
data Z
data S a
data Plus a b
newtype Finite s a = Finite {infinite :: [a]} deriving Show
instance Functor (Finite n) where
fmap f = Finite . fmap f . infinite
emp :: Finite Z a
emp = Finite []
(-:) :: a -> Finite n a -> Finite (S n) a
(-:) a l = Finite $ a : (infinite l)
infixr 5 -:
(++) :: Finite s1 a -> Finite s2 a -> Finite (S (Plus s1 s2)) a
(++) (Finite a) (Finite b) = Finite $ a Prelude.++ b
infixr 5 ++
map = fmap
/J
2010/10/13 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
>>
>
>
>
> --
> Eugene Kirpichov
> Senior Software Engineer,
> Grid Dynamics http://www.griddynamics.com/
> ___
> 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
Re: [Haskell-cafe] Finite but not fixed length...
infinite value is value, that have no upper bound (see infinity
definition). So, you have to provide upper bound at compile time. Tree
example provides such bound.
On 10/13/2010 03:27 PM, Eugene Kirpichov wrote:
> Again, the question is not how to arrange that all non-bottom values
> are finite: this can easily be done using strictness, as in your List
> example.
>
> The trick is to reject infinite values in compile time. How can *this* be
> done?
>
> 13 октября 2010 г. 15:26 пользователь Permjacov Evgeniy
> написал:
>> On 10/13/2010 03:09 PM, Eugene Kirpichov wrote:
>>
>> 1-st scenario: If you have, for example, 2-3 tree, it definitly has a
>> root. If you construct tree from list and then match over root, the
>> entire tree (and entire source list) will be forced. And on every
>> update, 2-3 tree's root is reconstructed in functional setting. So, if
>> you'll try to build 2-3 tree from infinite list, it will fail in process
>> due insuffisient memory.
>> Of course, you can make the same with
>> data List a = Cons a (!List a) | Nil
>>
>> second scenario
>> data Node a = Nil | One a | Two a a
>> and so Node (Node (Node (Node a))) has at most 2^4 = 16 elements. with
>> some triks you'll be able to set upper bound in runtime.
>>
>>> I don't see how. Could you elaborate?
>>>
>>> 13 октября 2010 г. 14:46 пользователь Permjacov Evgeniy
>>> написал:
On 10/13/2010 12:33 PM, Eugene Kirpichov wrote:
I think, tree-like structure, used as sequence (like fingertrees), will
do the work.
> 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
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Finite but not fixed length...
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
Re: [Haskell-cafe] Finite but not fixed length...
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
>>>
>>
>>
>
--
Eugene Kirpichov
Senior Software Engineer,
Grid Dynamics http://www.griddynamics.com/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Finite but not fixed length...
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
Re: [Haskell-cafe] Finite but not fixed length...
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
>
--
Eugene Kirpichov
Senior Software Engineer,
Grid Dynamics http://www.griddynamics.com/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Finite but not fixed length...
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
Re: [Haskell-cafe] Finite but not fixed length...
On 13 October 2010 08:57, Jason Dusek wrote: > Is there a way to write a Haskell data structure that is > necessarily only one or two or seventeen items long; but > that is nonetheless statically guaranteed to be of finite > length? Maybe you want a list whose denotation is formed by a least (rather than a greatest) fixed point? i.e. the type of spine-strict lists: """ data FinList a = Nil | Cons a !(FinList a) deriving (Show) ones_fin = 1 `Cons` ones_fin take_fin n Nil = Nil take_fin n (Cons x rest) | n <= 0= Nil | otherwise = Cons x (take_fin (n - 1) rest) ones = 1 : ones main = do print $ take 5 ones print $ take_fin 5 ones_fin """ If you have e :: FinList a then if e /= _|_ it is necessarily of finite length. Max ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Finite but not fixed length...
Hm. This is not actually an answer to your question, just a
"discussion starter", but still.
The code below typechecks, though actually it shouldn't: there's no
type "n" such that "ones" is formed by the FL from some value of type
List Int n.
Or should it?
{-# 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
2010/10/13 Jason Dusek :
> Is there a way to write a Haskell data structure that is
> necessarily only one or two or seventeen items long; but
> that is nonetheless statically guaranteed to be of finite
> length?
>
> --
> Jason Dusek
> Linux User #510144 | http://counter.li.org/
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
--
Eugene Kirpichov
Senior Software Engineer,
Grid Dynamics http://www.griddynamics.com/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Finite but not fixed length...
Is there a way to write a Haskell data structure that is necessarily only one or two or seventeen items long; but that is nonetheless statically guaranteed to be of finite length? -- Jason Dusek Linux User #510144 | http://counter.li.org/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
