Ashley Yakeley <[EMAIL PROTECTED]> writes: [...]
> -- which of these types are the same? > f1 = MkFoo undefined :: Foo Succ; > f2 = MkFoo undefined :: Foo Succ'; > f3 = MkFoo undefined :: Foo Succ''; > f4 = MkFoo undefined :: Foo (Add (Succ Zero)); yeah, why not! Have them all be the same thing. (i added the missing "Foo" on f4) add Zero b = b add (Succ a) b = Succ (add a b) mult Zero b = Zero mult (Succ a) b = add b (mult a b) fact Zero = Zero fact (Succ n) = mult (Succ n) (fact n) data Foo f = MkFoo (f ()) succ' = Succ succ'' n = Succ n -- which of these types are the same? f1 = MkFoo undefined :: Foo Succ f2 = MkFoo undefined :: Foo succ' f3 = MkFoo undefined :: Foo succ'' f4 = MkFoo undefined :: Foo (add (Succ Zero)) add to haskell - eta-expanding of (add (Succ Zero)) in (\x -> add (Succ Zero) x) - compile-time evaluation of type expressions (handling unbounded parameters like "x" above) and that should do it! I don't think this is a crazy as it sounds. Cayenne has already started computing types at compile-time. I'm currently working on merd (http://merd.net) which has a such a type system. eg: range(n, m) = if n < m then n | range(n + 1, m) else n Two_to_height = range(2, 8) #=> 2|3|4|5|6|7|8 restricted_identity !! Two_to_height -> Two_to_height restricted_identity(x) = x restricted_identity(4) #=> 4 restricted_identity(1) #=> compile-time error: 1 is not in 2|3|4|5|6|7|8 _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell