Potentially untypable program

[Mathnerd314]

I guess HM with infinite types can type the example I gave at CCC today, but what about this?

I = {x->x};  
K = {x->{y->x}};  
W = {x->(x x)};  
term = {z->{y ->((y (z I))(z K))}};
test = (term W);
(test {x -> {y -> (pair (x 3) (((y "a") "b") "c")) } })

This uses test at a non-lambda value so should be incompatible with the deduced HM type you gave, { {A:{A->A} -> {A->B} } -> B }, that forces everything to be a lambda.
But of course it runs fine and produces (3,"b").

[cliffclick]

Two tests added based on Fridays CCC.  Here's the typing for the original I/K/W term: |  @test public void test78() {|| ||    rune("I = {x->x};"+|| ||         "K = {x->{y->x}};"+|| ||         "W = {x->(x x)};"+|| ||         "term = {z->{y ->((y (z I))(z K))}};"+|| ||         "test = (term W);"+|| ||         "test",|| ||         "{ { A:{A->A} -> {A->B} } -> B }",|| ||         "[22]{any,3 ->Scalar }",|| ||         null,"[19,22]");|| ||  }|| | |AA type: ||{ { A:{A -> A} -> {A                   ->B} } -> B } | |Haskel:    ( ||(a -> a) ->  (d -> c -> e -> c) -> b  ) -> b| |||| The two types are very similar, except for the infinite type for AA and the expansion term in Haskel.  Haskel uses System F, and I am allowing infinite types, so I've no idea if one type is "more principle" than another. Next you apply test with an argument: |{x -> {y -> (pair (x 3) (((y \"a\") \"b\") \"c\")) } }| |  @test public void test79() {|| ||    rune("I = {x->x};"+|| ||         "K = {x->{y->x}};"+|| ||         "W = {x->(x x)};"+|| ||         "term = {z->{y ->((y (z I))(z K))}};"+|| ||         "test = (term W);"+|| ||         "(test {x -> {y -> (pair (x 3) (((y \"a\") \"b\") \"c\")) } })",|| ||         "*(A:Cannot unify {A->A} and 3 and *str:(nint8), A)",|| ||         "*[7](^=any, Scalar, Scalar)",|| ||         "[4,7]","[]");|| ||  }|| | test's first argument is the self-recursive type A:{A->A}, which is a function which calls itself.  This ends up binding 'y' to the same type, and then this type is applied to 3 and some strings.  Since it expects a function, you get a pair of the error term: |(A:Cannot unify {A->A} and 3 and *str:(nint8), A)| Both programs agree that a pair should be returned, and AA's 2nd test is self-consistent with the derived type from the first expression. I'm guessing Haskel is "more right", and there's an AA bug. Can you send me the series of Haskel types for variations on a reduced "term"? |I = {x->x};||             // Maybe also for terms I,K,W although they look all right ||K = {x->{y->x}};|| ||W = {x->(x x)};|| ||{z->{y ->((y (z I))(z K))}}||  // Haskel type for this term, plus some smaller variants?| ||{z->{y ->((z I) (z K))}} || |||{z-> ((z I) (z K))} || | | | || Cliff

…

On 6/24/2022 4:21 PM, Mathnerd314 wrote: I guess HM with infinite types can type the example I gave at CCC today, but what about this? |I = {x->x}; K = {x->{y->x}}; W = {x->(x x)}; term = {z->{y ->((y (z I))(z K))}}; test = (term W); (test {x -> {y -> (pair (x 3) (((y "a") "b") "c")) } }) | This uses |test| at a non-lambda value so should be incompatible with the deduced HM type you gave, |{ {A:{A->A} -> {A->B} } -> B }|, that forces everything to be a lambda. But of course it runs fine and produces |(3,"b")|. — Reply to this email directly, view it on GitHub <#28>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAL3JYGE6FLNH3LWNNVZ623VQY7ITANCNFSM5ZZIC7CA>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[Mathnerd314]

Well, what I put for "Haskell type" is actually the type I think an intersection type system would infer. Haskell only came into play because I used it to infer the type of the fully reduced form, test = λ y . y (λ x . x) (λ y . λ x . λ y . x), since I don't have a working intersection type implementation. This uses the property of "subject expansion" that holds for intersection type systems (but not for Haskell's type system or most other type system) - subject expansion means that if term M reduces to term N, and N has type T, then M also has type T.

I worked out by hand the intersection types for your examples as follows, based on my reading of this paper:

Term	Type
I = {x->x}	a -> a
K = {x->{y->x}}	a -> b -> a
W = {x->(x x)}	((a -> b) ∩ a) -> b
term = {z->{y ->((y (z I))(z K))}}	(((a -> a) -> d) ∩ ((b -> c -> b) -> e)) -> (d -> e -> f) -> f
test = (term W)	(a -> a) -> (d -> c -> e -> c) -> b ) -> b
(test {x -> {y -> (pair (x 3) (((y "a") "b") "c")	(Int, String)
{z->{y ->((z I) (z K))}}	(((d -> d) -> e -> c) ∩ ((a -> b -> a) -> e)) -> f -> c
{z-> ((z I) (z K))}	(((a -> a) -> c -> b) ∩ ((d -> e -> d) -> c)) -> b

I don't think failure of your algorithm on these examples necessarily means there's an AA bug. I've seen an argument that the semantics of these programs are confusing and that static type systems ruling them out make programs easier to understand. But it is true that these examples work in an untyped semantics, so they show that your system cannot type all successfully-running programs.

[cliffclick]

Will take a look tomorrow (the other bug was minor, but got social activities distracted so not done yet), but in this case |test| is being as a lambda in an application so a-priori looks fine to me. Will let you know once I pass it thru the typer. Cliff

…

On 6/24/2022 4:21 PM, Mathnerd314 wrote: I guess HM with infinite types can type the example I gave at CCC today, but what about this? |I = {x->x}; K = {x->{y->x}}; W = {x->(x x)}; term = {z->{y ->((y (z I))(z K))}}; test = (term W); (test {x -> {y -> (pair (x 3) (((y "a") "b") "c")) } }) | This uses |test| at a non-lambda value so should be incompatible with the deduced HM type you gave, |{ {A:{A->A} -> {A->B} } -> B }|, that forces everything to be a lambda. But of course it runs fine and produces |(3,"b")|. — Reply to this email directly, view it on GitHub <#28>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAL3JYGE6FLNH3LWNNVZ623VQY7ITANCNFSM5ZZIC7CA>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>