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

Reply via email to