On Sun, Feb 20, 2011 at 6:01 PM, Job Vranish <[email protected]> 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 <[email protected]> wrote: >> >> On Sat, Feb 14, 2009 at 2:06 PM, Job Vranish <[email protected]> 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 <[email protected]> wrote: >>> > On Fri, Feb 13, 2009 at 4:04 PM, Luke Palmer <[email protected]> >>> > wrote: >>> >> >>> >> On Fri, Feb 13, 2009 at 3:13 PM, Job Vranish <[email protected]> >>> >> 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.html >>> >>> >>> >>> 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 >>> >>> [email protected] >>> >>> http://www.haskell.org/mailman/listinfo/haskell-cafe >>> >> >>> > >>> > >> > > > _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
