Infinite types should be optionally allowed

Job Vranish

13 Feb 2009 13 Feb '09

10:13 p.m.

There are good reasons against allowing infinite types by default (mostly, that a lot of things type check that are normally not what we want). An old haskell cafe conversation on the topic is here: http://www.nabble.com/There%27s-nothing-wrong-with-infinite-types!-td7713737... However, I think infinite types should be allowed, but only with an explicit type signature. In other words, don't allow infinite types to be inferred, but if they are specified, let them pass. I think it would be very hard to shoot yourself in the foot this way. Newtype is the standard solution to situations where you really need an infinite type, but in some cases this can be a big annoyance. Using newtype sacrifices data type abstraction and very useful type classes like Functor. You can use multiparameter type classes and functional dependencies to recover some of the lost abstraction, but then type checking becomes harder to reason about and the code gets way more ugly (If you doubt, let me know, I have some examples). Allowing infinite types would fix this. I'm imagining a syntax something like this: someFunctionThatCreatesInfiniteType :: a -> b | b = [(a, b)] Thoughts? Opinions? Am I missing anything obvious? - Job

Show replies by date

Luke Palmer

13 Feb 13 Feb

11:04 p.m.

On Fri, Feb 13, 2009 at 3:13 PM, Job Vranish wrote:

...

There are good reasons against allowing infinite types by default (mostly, that a lot of things type check that are normally not what we want). An old haskell cafe conversation on the topic is here:

http://www.nabble.com/There%27s-nothing-wrong-with-infinite-types!-td7713737...http://www.nabble.com/There%27s-nothing-wrong-with-infinite-types%21-td77137...

However, I think infinite types should be allowed, but only with an explicit type signature. In other words, don't allow infinite types to be inferred, but if they are specified, let them pass. I think it would be very hard to shoot yourself in the foot this way.

That inference engine seems to be a pretty little proof-of-concept, doesn't it? But it is sweeping some very important stuff under the carpet. The proposal is to infer the type of a term, then check it against an annotation. Thus every program is well-typed, but it's the compiler's job to check that it has the type the user intended. I like the idea. But the inference engine is only half of the story. It does no type checking. Although checking is often viewed as the easier of the two problems, in this case it is not. A term has no normal form if and only if its type is equal to (forall a. a). You can see the problem here. Luke

...

Newtype is the standard solution to situations where you really need an infinite type, but in some cases this can be a big annoyance. Using newtype sacrifices data type abstraction and very useful type classes like Functor. You can use multiparameter type classes and functional dependencies to recover some of the lost abstraction, but then type checking becomes harder to reason about and the code gets way more ugly (If you doubt, let me know, I have some examples). Allowing infinite types would fix this.

I'm imagining a syntax something like this: someFunctionThatCreatesInfiniteType :: a -> b | b = [(a, b)]

Thoughts? Opinions? Am I missing anything obvious?

- Job _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Luke Palmer

11:09 p.m.

On Fri, Feb 13, 2009 at 4:04 PM, Luke Palmer wrote:

...

On Fri, Feb 13, 2009 at 3:13 PM, Job Vranish wrote:

...
There are good reasons against allowing infinite types by default (mostly, that a lot of things type check that are normally not what we want). An old haskell cafe conversation on the topic is here:

http://www.nabble.com/There%27s-nothing-wrong-with-infinite-types!-td7713737...http://www.nabble.com/There%27s-nothing-wrong-with-infinite-types%21-td77137...

However, I think infinite types should be allowed, but only with an explicit type signature. In other words, don't allow infinite types to be inferred, but if they are specified, let them pass. I think it would be very hard to shoot yourself in the foot this way.

Oops! I'm sorry, I completely misread the proposal. Or read it correctly, saw an undecidability hiding in there, and got carried away. What you are proposing is called equi-recursive types, in contrast to the more popular iso-recursive types (which Haskell uses). There are plentiful undecidable problems with equi-recursive types, but there are ways to pull it off. The question is whether these ways play nicely with Haskell's type system. But because of the fundamental computational problems associated, there needs to be a great deal of certainty that this is even possible before considering its language design implications.

...

That inference engine seems to be a pretty little proof-of-concept, doesn't it? But it is sweeping some very important stuff under the carpet.

The proposal is to infer the type of a term, then check it against an annotation. Thus every program is well-typed, but it's the compiler's job to check that it has the type the user intended. I like the idea.

But the inference engine is only half of the story. It does no type checking. Although checking is often viewed as the easier of the two problems, in this case it is not. A term has no normal form if and only if its type is equal to (forall a. a). You can see the problem here.

Luke

...
Newtype is the standard solution to situations where you really need an infinite type, but in some cases this can be a big annoyance. Using newtype sacrifices data type abstraction and very useful type classes like Functor. You can use multiparameter type classes and functional dependencies to recover some of the lost abstraction, but then type checking becomes harder to reason about and the code gets way more ugly (If you doubt, let me know, I have some examples). Allowing infinite types would fix this.

I'm imagining a syntax something like this: someFunctionThatCreatesInfiniteType :: a -> b | b = [(a, b)]

Thoughts? Opinions? Am I missing anything obvious?

- Job _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Job Vranish

14 Feb 14 Feb

9:06 p.m.

I'm pretty sure that the problem is decidable, at least with haskell 98 types (other type extensions may complicate things a bit). It ends up being a graph unification algorithm. I've tried some simple algorithms and they seem to work. What do you mean by "the inference engine is only half of the story"?

...

From what I understand, the inference engine infers types via unification, if the types unify, then the unified types are the inferred types, if the types don't unify, then type check fails. Am I missing/misunderstanding something?

I almost think that the problem might be solvable by just generating the appropriate newtype whenever an infinite type shows up, and doing the wrapping/unwrapping behind the scenes. This would be a hacked up way to do it, but I think it would work. On Fri, Feb 13, 2009 at 6:09 PM, Luke Palmer wrote:

...

On Fri, Feb 13, 2009 at 4:04 PM, Luke Palmer wrote:

...
On Fri, Feb 13, 2009 at 3:13 PM, Job Vranish wrote:

...
There are good reasons against allowing infinite types by default (mostly, that a lot of things type check that are normally not what we want). An old haskell cafe conversation on the topic is here:

http://www.nabble.com/There%27s-nothing-wrong-with-infinite-types!-td7713737...

However, I think infinite types should be allowed, but only with an explicit type signature. In other words, don't allow infinite types to be inferred, but if they are specified, let them pass. I think it would be very hard to shoot yourself in the foot this way.

Oops! I'm sorry, I completely misread the proposal. Or read it correctly, saw an undecidability hiding in there, and got carried away.

What you are proposing is called equi-recursive types, in contrast to the more popular iso-recursive types (which Haskell uses). There are plentiful undecidable problems with equi-recursive types, but there are ways to pull it off. The question is whether these ways play nicely with Haskell's type system.

But because of the fundamental computational problems associated, there needs to be a great deal of certainty that this is even possible before considering its language design implications.

...
That inference engine seems to be a pretty little proof-of-concept, doesn't it? But it is sweeping some very important stuff under the carpet.

The proposal is to infer the type of a term, then check it against an annotation. Thus every program is well-typed, but it's the compiler's job to check that it has the type the user intended. I like the idea.

But the inference engine is only half of the story. It does no type checking. Although checking is often viewed as the easier of the two problems, in this case it is not. A term has no normal form if and only if its type is equal to (forall a. a). You can see the problem here.

Luke

...
Newtype is the standard solution to situations where you really need an infinite type, but in some cases this can be a big annoyance. Using newtype sacrifices data type abstraction and very useful type classes like Functor. You can use multiparameter type classes and functional dependencies to recover some of the lost abstraction, but then type checking becomes harder to reason about and the code gets way more ugly (If you doubt, let me know, I have some examples). Allowing infinite types would fix this.

I'm imagining a syntax something like this: someFunctionThatCreatesInfiniteType :: a -> b | b = [(a, b)]

Thoughts? Opinions? Am I missing anything obvious?

- Job _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Luke Palmer

16 Feb 16 Feb

10:16 p.m.

On Sat, Feb 14, 2009 at 2:06 PM, Job Vranish wrote:

...

I'm pretty sure that the problem is decidable, at least with haskell 98 types (other type extensions may complicate things a bit). It ends up being a graph unification algorithm. I've tried some simple algorithms and they seem to work.

What do you mean by "the inference engine is only half of the story"? From what I understand, the inference engine infers types via unification, if the types unify, then the unified types are the inferred types, if the types don't unify, then type check fails. Am I missing/misunderstanding something?

Sorry it took me so long to respond. It took a while to formulate this example. Here are two (convoluted) functions, passed to the fixtypes inference engine: Expr> y (b (c i) (c (b b (b c (c i))))) (fix b . (a -> b -> (a -> c -> d) -> d) -> c) -> c Expr> y (b (c i) (b (c (b b (b c (c i)))) (b (c i) k))) (fix c . ((a -> ((b -> c) -> d) -> (a -> d -> e) -> e) -> f) -> f) These are somewhat complex types; sorry about that. But here's a challenge: is one of these types more general than the other? For example, if you wrote the first term and gave the second signature, should it typecheck? If you figure it out, can you give an algorithm for doing so? I'm not going to say how I came up with these functions, because that would give away the answer :-) Luke

...

I almost think that the problem might be solvable by just generating the appropriate newtype whenever an infinite type shows up, and doing the wrapping/unwrapping behind the scenes. This would be a hacked up way to do it, but I think it would work.

...
On Fri, Feb 13, 2009 at 4:04 PM, Luke Palmer wrote:

...
On Fri, Feb 13, 2009 at 3:13 PM, Job Vranish

wrote:

...
...
There are good reasons against allowing infinite types by default (mostly, that a lot of things type check that are normally not what we want). An old haskell cafe conversation on the topic is here:

http://www.nabble.com/There%27s-nothing-wrong-with-infinite-types!-td7713737...http://www.nabble.com/There%27s-nothing-wrong-with-infinite-types%21-td77137...

...
However, I think infinite types should be allowed, but only with an explicit type signature. In other words, don't allow infinite types to be inferred, but if they are specified, let them pass. I think it would be very hard to shoot yourself in the foot this way.

Oops! I'm sorry, I completely misread the proposal. Or read it correctly, saw an undecidability hiding in there, and got carried away.

What you are proposing is called equi-recursive types, in contrast to the more popular iso-recursive types (which Haskell uses). There are

...
undecidable problems with equi-recursive types, but there are ways to

On Fri, Feb 13, 2009 at 6:09 PM, Luke Palmer wrote: plentiful pull

...
it off. The question is whether these ways play nicely with Haskell's type system.

But because of the fundamental computational problems associated, there needs to be a great deal of certainty that this is even possible before considering its language design implications.

...
That inference engine seems to be a pretty little proof-of-concept, doesn't it? But it is sweeping some very important stuff under the

carpet.

...
The proposal is to infer the type of a term, then check it against an annotation. Thus every program is well-typed, but it's the compiler's

job

...
to check that it has the type the user intended. I like the idea.

But the inference engine is only half of the story. It does no type checking. Although checking is often viewed as the easier of the two problems, in this case it is not. A term has no normal form if and only if its type is equal to (forall a. a). You can see the problem here.

Luke

...
Newtype is the standard solution to situations where you really need an infinite type, but in some cases this can be a big annoyance. Using newtype sacrifices data type abstraction and very useful type classes like Functor. You can use multiparameter type classes and functional dependencies to recover some of the lost abstraction, but then type checking becomes harder to reason about and the code gets way more ugly (If you doubt, let me know, I have some examples). Allowing infinite types would fix this.

I'm imagining a syntax something like this: someFunctionThatCreatesInfiniteType :: a -> b | b = [(a, b)]

Thoughts? Opinions? Am I missing anything obvious?

- Job _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Job Vranish

21 Feb 21 Feb

1:01 a.m.

Sorry for bringing back an ancient thread but I'd still like to understand this better. It is still not obvious to me why typechecking infinite types is so hard. Is determining type 'equivalence' the hard part? or is that a separate issue? I wrote a simple infinite type inferer and made an attempt at an algorithm that can answer your question. The algorithm works like this: Given two types *a* and *b*: unify *a* with * b*, if the resulting type is 'equivalent' to the original *a,* then *b* must be (I think) at least as general as *a*. To determine equivalence, I start with the head of both types (which are represented as graphs) and check to see if the constructors are the same. If they are then I set those two nodes 'equal' and recurse with the children. It's a 'destructive' algorithm that effectively 'zips' the two graphs together. It returns false if it encounters two constructors that are different. My current algorithm says that neither of the types you gave is strictly more general than the other, which I'm guessing is probably not true. I'm curious what the correct answer is and would appreciate someone pointing out the flaw in my reasoning/code :) My test code is on github here: https://github.com/jvranish/InfiniteTypes Also, is there a book you'd recommend that would explain this in further detail? Thanks, - Job On Mon, Feb 16, 2009 at 5:16 PM, Luke Palmer wrote:

...

On Sat, Feb 14, 2009 at 2:06 PM, Job Vranish wrote:

...
I'm pretty sure that the problem is decidable, at least with haskell 98 types (other type extensions may complicate things a bit). It ends up being a graph unification algorithm. I've tried some simple algorithms and they seem to work.

What do you mean by "the inference engine is only half of the story"? From what I understand, the inference engine infers types via unification, if the types unify, then the unified types are the inferred types, if the types don't unify, then type check fails. Am I missing/misunderstanding something?

Sorry it took me so long to respond. It took a while to formulate this example.

Here are two (convoluted) functions, passed to the fixtypes inference engine:

Expr> y (b (c i) (c (b b (b c (c i))))) (fix b . (a -> b -> (a -> c -> d) -> d) -> c) -> c Expr> y (b (c i) (b (c (b b (b c (c i)))) (b (c i) k))) (fix c . ((a -> ((b -> c) -> d) -> (a -> d -> e) -> e) -> f) -> f)

These are somewhat complex types; sorry about that. But here's a challenge: is one of these types more general than the other? For example, if you wrote the first term and gave the second signature, should it typecheck? If you figure it out, can you give an algorithm for doing so?

I'm not going to say how I came up with these functions, because that would give away the answer :-)

Luke

...
I almost think that the problem might be solvable by just generating the appropriate newtype whenever an infinite type shows up, and doing the wrapping/unwrapping behind the scenes. This would be a hacked up way to do it, but I think it would work.

...
On Fri, Feb 13, 2009 at 4:04 PM, Luke Palmer wrote:

...
On Fri, Feb 13, 2009 at 3:13 PM, Job Vranish

wrote:

...
...
There are good reasons against allowing infinite types by default (mostly, that a lot of things type check that are normally not what we want). An old haskell cafe conversation on the topic is here:

http://www.nabble.com/There%27s-nothing-wrong-with-infinite-types!-td7713737...http://www.nabble.com/There%27s-nothing-wrong-with-infinite-types%21-td77137...

...
However, I think infinite types should be allowed, but only with an explicit type signature. In other words, don't allow infinite types to be inferred, but if they are specified, let them pass. I think it would be very hard to shoot yourself in the foot this way.

Oops! I'm sorry, I completely misread the proposal. Or read it correctly, saw an undecidability hiding in there, and got carried away.

What you are proposing is called equi-recursive types, in contrast to

...
more popular iso-recursive types (which Haskell uses). There are

...
undecidable problems with equi-recursive types, but there are ways to

On Fri, Feb 13, 2009 at 6:09 PM, Luke Palmer wrote: the plentiful pull

...
it off. The question is whether these ways play nicely with Haskell's type system.

But because of the fundamental computational problems associated, there needs to be a great deal of certainty that this is even possible before considering its language design implications.

...
That inference engine seems to be a pretty little proof-of-concept, doesn't it? But it is sweeping some very important stuff under the

carpet.

...
The proposal is to infer the type of a term, then check it against an annotation. Thus every program is well-typed, but it's the compiler's

job

...
to check that it has the type the user intended. I like the idea.

But the inference engine is only half of the story. It does no type checking. Although checking is often viewed as the easier of the two problems, in this case it is not. A term has no normal form if and only if its type is equal to (forall a. a). You can see the problem here.

Luke

...
Newtype is the standard solution to situations where you really need an infinite type, but in some cases this can be a big annoyance. Using newtype sacrifices data type abstraction and very useful type classes like Functor. You can use multiparameter type classes and functional dependencies to recover some of the lost abstraction, but then type checking becomes harder to reason about and the code gets way more ugly (If you doubt, let me know, I have some examples). Allowing infinite types would fix this.

I'm imagining a syntax something like this: someFunctionThatCreatesInfiniteType :: a -> b | b = [(a, b)]

Thoughts? Opinions? Am I missing anything obvious?

- Job _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Brandon Moore

1:56 a.m.

...

From: Job Vranish

Sorry for bringing back an ancient thread but I'd still like to understand this

...

better.

It is still not obvious to me why typechecking infinite types is so hard. Is determining type 'equivalence' the hard part? or is that a separate issue?

Typechecking with regular types isn't hard. The problem is, the type system is almost useless for catching bad programs. Every closed lambda expression is typeable if infinite types are allowed. Usually systems add some sort of ad-hoc restriction on regular types, like requiring that all all cycles pass through a record type.

...

The algorithm works like this: Given two types a and b: unify a with b, if the resulting type is 'equivalent' to the original a, then b must be (I think) at least as general as a.

To determine equivalence, I start with the head of both types (which are represented as graphs) and check to see if the constructors are the same. If they are then I set those two nodes 'equal' and recurse with the children. It's a 'destructive' algorithm that effectively 'zips' the two graphs together.

...

It returns false if it encounters two constructors that are different.

I have also found that destructive graph-based unification is the easiest way to work with recursive types. Brandon

Job Vranish

3:23 p.m.

On Sun, Feb 20, 2011 at 8:56 PM, Brandon Moore wrote:

...

Typechecking with regular types isn't hard.

So do I have the right idea then? To check against a signature, I can just unify the two types and then check if the unified type is 'equivalent' (is there a special word for this kind of equivalence?) to the original signature? I've gotten the impression from multiple people that type checking with infinite types is hard. Maybe this isn't so?

...

The problem is, the type system is almost useless for catching bad programs. Every closed lambda expression is typeable if infinite types are allowed.

Yes, this part I understand quite well :) Usually systems add some sort of ad-hoc restriction on regular types, like requiring that all all cycles

...

pas through

a record type. Yeah, what I really want is just a better ad-hoc restriction or annotation. I quite routinely work with code that would be much more simple and elegant with infinite types. - Job

Brandon Moore

3:38 p.m.

...

From: Job Vranish On Sun, Feb 20, 2011 at 8:56 PM, Brandon Moore wrote:

...
Typechecking with regular types isn't hard.

...

So do I have the right idea then? To check against a signature, I can just unify

the two types and then check if the unified type is 'equivalent' (is there a special word for this kind of equivalence?) to the original signature? I've gotten the impression from multiple people that type checking with infinite

types is hard. Maybe this isn't so?

I haven't thought about checking against signatures. I think what you do is replace all the variables in the signature with Skolem constants, and unify the inferred type against that. There may be more complications if type inference is directed by the signature.

...

...
Usually systems add some sort ofad-hoc restriction on regular types, like requiring that all all cycles pas through a record type.

Yeah, what I really want is just a better ad-hoc restriction or annotation. I quite routinely work with code that would be much more simple and elegant with infinite types.

The restrictions I mentioned are supposed to allow using recursive record types to build an object system. It sounds like you want to allow infinite types only as specified by signatures. I think you could take a signature with explicit recursion, label those indicated cycles as allowed, somehow propagate the labels during unification, and check that the only cycles that appear are those specifically licensed by the signature. Brandon

Luke Palmer

9:54 p.m.

On Sun, Feb 20, 2011 at 6:01 PM, Job Vranish wrote:

...

My current algorithm says that neither of the types you gave is strictly more general than the other, which I'm guessing is probably not true. I'm curious what the correct answer is and would appreciate someone pointing out the flaw in my reasoning/code :)

I don't remember how I constructed those terms, and I admit that I was arguing out of my depth. I really should have exposed my construction -- we're all good engineers here, we know the difference between an algorithm and intuition. Things I have read since have suggested that I was wrong. Pierce's Types and Programming Languages has a chapter on equi-recursive types which, if it does not provide insight itself, I'm sure has references to papers that go into all the detail needed to answer this technical question. Luke

...

My test code is on github here: https://github.com/jvranish/InfiniteTypes Also, is there a book you'd recommend that would explain this in further detail? Thanks, - Job

On Mon, Feb 16, 2009 at 5:16 PM, Luke Palmer wrote:

...
On Sat, Feb 14, 2009 at 2:06 PM, Job Vranish wrote:

...
I'm pretty sure that the problem is decidable, at least with haskell 98 types (other type extensions may complicate things a bit). It ends up being a graph unification algorithm. I've tried some simple algorithms and they seem to work.

What do you mean by "the inference engine is only half of the story"? From what I understand, the inference engine infers types via unification, if the types unify, then the unified types are the inferred types, if the types don't unify, then type check fails. Am I missing/misunderstanding something?

Sorry it took me so long to respond. It took a while to formulate this example.

Here are two (convoluted) functions, passed to the fixtypes inference engine:

Expr> y (b (c i) (c (b b (b c (c i))))) (fix b . (a -> b -> (a -> c -> d) -> d) -> c) -> c Expr> y (b (c i) (b (c (b b (b c (c i)))) (b (c i) k))) (fix c . ((a -> ((b -> c) -> d) -> (a -> d -> e) -> e) -> f) -> f)

These are somewhat complex types; sorry about that. But here's a challenge: is one of these types more general than the other? For example, if you wrote the first term and gave the second signature, should it typecheck? If you figure it out, can you give an algorithm for doing so?

I'm not going to say how I came up with these functions, because that would give away the answer :-)

Luke

...
I almost think that the problem might be solvable by just generating the appropriate newtype whenever an infinite type shows up, and doing the wrapping/unwrapping behind the scenes. This would be a hacked up way to do it, but I think it would work.

On Fri, Feb 13, 2009 at 6:09 PM, Luke Palmer wrote:

...
On Fri, Feb 13, 2009 at 4:04 PM, Luke Palmer wrote:

...
On Fri, Feb 13, 2009 at 3:13 PM, Job Vranish wrote:

...
There are good reasons against allowing infinite types by default (mostly, that a lot of things type check that are normally not what we want). An old haskell cafe conversation on the topic is here:

http://www.nabble.com/There%27s-nothing-wrong-with-infinite-types!-td7713737...

However, I think infinite types should be allowed, but only with an explicit type signature. In other words, don't allow infinite types to be inferred, but if they are specified, let them pass. I think it would be very hard to shoot yourself in the foot this way.

Oops! I'm sorry, I completely misread the proposal. Or read it correctly, saw an undecidability hiding in there, and got carried away.

What you are proposing is called equi-recursive types, in contrast to the more popular iso-recursive types (which Haskell uses). There are plentiful undecidable problems with equi-recursive types, but there are ways to pull it off. The question is whether these ways play nicely with Haskell's type system.

But because of the fundamental computational problems associated, there needs to be a great deal of certainty that this is even possible before considering its language design implications.

...
That inference engine seems to be a pretty little proof-of-concept, doesn't it? But it is sweeping some very important stuff under the carpet.

The proposal is to infer the type of a term, then check it against an annotation. Thus every program is well-typed, but it's the compiler's job to check that it has the type the user intended. I like the idea.

But the inference engine is only half of the story. It does no type checking. Although checking is often viewed as the easier of the two problems, in this case it is not. A term has no normal form if and only if its type is equal to (forall a. a). You can see the problem here.

Luke

...
Newtype is the standard solution to situations where you really need an infinite type, but in some cases this can be a big annoyance. Using newtype sacrifices data type abstraction and very useful type classes like Functor. You can use multiparameter type classes and functional dependencies to recover some of the lost abstraction, but then type checking becomes harder to reason about and the code gets way more ugly (If you doubt, let me know, I have some examples). Allowing infinite types would fix this.

I'm imagining a syntax something like this: someFunctionThatCreatesInfiniteType :: a -> b | b = [(a, b)]

Thoughts? Opinions? Am I missing anything obvious?

- Job _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Job Vranish

22 Feb 22 Feb

5:55 p.m.

Thanks, Perhaps my algorithm works then. I shall have to read up more on these things :) - Job On Mon, Feb 21, 2011 at 4:54 PM, Luke Palmer wrote:

...

On Sun, Feb 20, 2011 at 6:01 PM, Job Vranish wrote:

...
My current algorithm says that neither of the types you gave is strictly more general than the other, which I'm guessing is probably not true. I'm curious what the correct answer is and would appreciate someone pointing out the flaw in my reasoning/code :)

I don't remember how I constructed those terms, and I admit that I was arguing out of my depth. I really should have exposed my construction -- we're all good engineers here, we know the difference between an algorithm and intuition.

Things I have read since have suggested that I was wrong. Pierce's Types and Programming Languages has a chapter on equi-recursive types which, if it does not provide insight itself, I'm sure has references to papers that go into all the detail needed to answer this technical question.

Luke

...
My test code is on github here: https://github.com/jvranish/InfiniteTypes Also, is there a book you'd recommend that would explain this in further detail? Thanks, - Job

On Mon, Feb 16, 2009 at 5:16 PM, Luke Palmer wrote:

...
On Sat, Feb 14, 2009 at 2:06 PM, Job Vranish

...
...
I'm pretty sure that the problem is decidable, at least with haskell 98 types (other type extensions may complicate things a bit). It ends up being a graph unification algorithm. I've tried some simple algorithms and they seem to work.

What do you mean by "the inference engine is only half of the story"? From what I understand, the inference engine infers types via unification, if the types unify, then the unified types are the inferred types, if the types don't unify, then type check fails. Am I missing/misunderstanding something?

Sorry it took me so long to respond. It took a while to formulate this example.

Here are two (convoluted) functions, passed to the fixtypes inference engine:

Expr> y (b (c i) (c (b b (b c (c i))))) (fix b . (a -> b -> (a -> c -> d) -> d) -> c) -> c Expr> y (b (c i) (b (c (b b (b c (c i)))) (b (c i) k))) (fix c . ((a -> ((b -> c) -> d) -> (a -> d -> e) -> e) -> f) -> f)

These are somewhat complex types; sorry about that. But here's a challenge: is one of these types more general than the other? For example, if you wrote the first term and gave the second signature, should it typecheck? If you figure it out, can you give an algorithm for doing so?

I'm not going to say how I came up with these functions, because that would give away the answer :-)

Luke

...
I almost think that the problem might be solvable by just generating the appropriate newtype whenever an infinite type shows up, and doing the wrapping/unwrapping behind the scenes. This would be a hacked up way to do it, but I think it would work.

On Fri, Feb 13, 2009 at 6:09 PM, Luke Palmer

wrote:

...
...
On Fri, Feb 13, 2009 at 4:04 PM, Luke Palmer wrote:

...
On Fri, Feb 13, 2009 at 3:13 PM, Job Vranish wrote: > > There are good reasons against allowing infinite types by default > (mostly, that a lot of things type check that are normally not what > we > want). An old haskell cafe conversation on the topic is here: > > >

http://www.nabble.com/There%27s-nothing-wrong-with-infinite-types!-td7713737...

...
> > However, I think infinite types should be allowed, but only with an > explicit type signature. In other words, don't allow infinite types > to > be inferred, but if they are specified, let them pass. I think it > would be very hard to shoot yourself in the foot this way.

Oops! I'm sorry, I completely misread the proposal. Or read it correctly, saw an undecidability hiding in there, and got carried away.

What you are proposing is called equi-recursive types, in contrast to the more popular iso-recursive types (which Haskell uses). There are plentiful undecidable problems with equi-recursive types, but there are ways to pull it off. The question is whether these ways play nicely with Haskell's type system.

But because of the fundamental computational problems associated,

wrote: there

...
...
...
needs to be a great deal of certainty that this is even possible before considering its language design implications.

...
That inference engine seems to be a pretty little proof-of-concept, doesn't it? But it is sweeping some very important stuff under the carpet.

The proposal is to infer the type of a term, then check it against

an

...
annotation. Thus every program is well-typed, but it's the compiler's job to check that it has the type the user intended. I like the idea.

But the inference engine is only half of the story. It does no type checking. Although checking is often viewed as the easier of the two problems, in this case it is not. A term has no normal form if and only if its type is equal to (forall a. a). You can see the problem here.

Luke

> > > Newtype is the standard solution to situations where you really need > an infinite type, but in some cases this can be a big annoyance. > Using > newtype sacrifices data type abstraction and very useful type classes > like Functor. You can use multiparameter type classes and functional > dependencies to recover some of the lost abstraction, but then type > checking becomes harder to reason about and the code gets way more > ugly (If you doubt, let me know, I have some examples). Allowing > infinite types would fix this. > > I'm imagining a syntax something like this: > someFunctionThatCreatesInfiniteType :: a -> b | b = [(a, b)] > > Thoughts? Opinions? Am I missing anything obvious? > > - Job > _______________________________________________ > 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

5248

Age (days ago)

5987

Last active (days ago)

List overview

Download

10 comments

3 participants

participants (3)

Brandon Moore
Job Vranish
Luke Palmer