Hakaru file test fails with "Missing common type" error

[GenevaS]

When using the testConcreteFiles function from hakaru/haskell/Tests/TestTools, a "Missing common type" error occurs for some files. We cannot figure out where this error is being triggered from. Test t14 is an example which has this problem:

### Failure in: 6:RoundTrip:2:7:t14
    haskell\Tests\TestTools.hs:133
    "Missing common type:\n\n    
4| (match x1: \n    
5|   true: \n    
6|    x0 <~ x0 <~ categorical([(3 / 5),\n    
7|                             real2prob((prob2real(1) - prob2real((3 / 5))))])\n    
8|          return [true, false][x0]\n    
9|    return (match x0: \n   
10|             true: 37\n   
11|             false: 42)\n   
12|   false: \n   
13|    x0 <~ x0 <~ categorical([(2 / 7),\n   
14|                             real2prob((prob2real(1) - prob2real((2 / 7))))])\n   
15|          return [true, false][x0]\n   
16|    (match x0: \n   
17|      true: uniform(10, 12)\n   
18|      false: uniform(14, 16)))\nNo lub of types SMeasure SNat and SMeasure SReal"

[JacquesCarette]

This definitely looks like a bug (in the printer?). Looks like 37 and 42 should be cast to real, to match the other clause.

[zaxtax]

That does look weird. I'll look into it later.

On Tue, Jun 20, 2017 at 4:42 PM, Jacques Carette notifications@github.com wrote:

This definitely looks like a bug (in the printer?). Looks like 37 and 42 should be cast to real, to match the other clause.

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/hakaru-dev/hakaru/issues/90#issuecomment-309885231, or mute the thread https://github.com/notifications/unsubscribe-auth/AAAhUS7fJ-9u3FyY2Ylmq9XzBe2PGBa6ks5sGC6kgaJpZM4OAIEL .

[yuriy0]

A quick search reveals the error comes from missingLub. That function is used in inferLubType and inferCaseLax. I would guess the error comes from inferLubType, which occurs in quite a number of places.

[JacquesCarette]

That is where it comes from, yes. But what it means is that Measure Nat and Measure Real have no common (smallest) super-type. Because they are incomparable (one is essentially counting while the other is lebesgue).

The above piece of code is actually particularly nasty regarding inference and/or automatic coercion insertion.

[zaxtax]

So the issue is there is no way to unify measure(nat) and measure(real), but it shouldn't be getting to that point since uniform only takes real numbers.

On Tue, Jun 20, 2017 at 5:01 PM, yuriy0 notifications@github.com wrote:

A quick search reveals the error comes from missingLub https://github.com/hakaru-dev/hakaru/blob/5fa45c01c0ed8492350f6cc11205dc5e39f00cf3/haskell/Language/Hakaru/Syntax/TypeCheck.hs#L326. That function is used in inferLubType https://github.com/hakaru-dev/hakaru/blob/5fa45c01c0ed8492350f6cc11205dc5e39f00cf3/haskell/Language/Hakaru/Syntax/TypeCheck.hs#L1163 and inferCaseLax. I would guess the error comes from inferLubType, which occurs in quite a number of places.

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/hakaru-dev/hakaru/issues/90#issuecomment-309890342, or mute the thread https://github.com/notifications/unsubscribe-auth/AAAhUXSUkM3SrADt1jLE4WL7bI93DLPZks5sGDM4gaJpZM4OAIEL .

[ccshan]

This test should type check, because of the following reasoning.

• The expressions 37, 42, and match x0: true: 37 false: 42 all have all of the following types: nat, int, real, prob.
• So the expression return (match x0: true: 37 false: 42) has all of the following types: measure(nat), measure(int), measure(real), measure(prob).
• Moreover, the expressions uniform(10, 12) and uniform(14, 16) both have the type measure(real), so the expression match x0: true: uniform(10, 12) false: uniform(14, 16) does too.
• Given that both branches of match x1: ... have the type measure(real), the expression match x1: ... also has the type measure(real).

Not having studied bidirectional type checking formally, I believe the way our type checker should manage to type-check this test is as follows.

• To infer the type of match x1: ..., we first infer the type of its two branches. Type inference means finding the least type that an expression has, so the two types inferred are measure(nat) and measure(real) respectively.
• We join the types measure(nat) and measure(real) to get the type measure(real).
• We type-check the two branches at the joined type measure(real), so that literals such as 37 and 42 receive appropriate types (real rather than nat) and any necessary coercions are inserted (here we happen to not need any coercions).

It's not true that measure(nat) and measure(real) should be incomparable or should not unify. After all, we want each expression to have a principal type, and we want an expression such as return 37 to have both the type measure(nat) and the type measure(real) (because we want 37 to have both the type nat and the type real), so what is the principal type of return 37 if not measure(nat)?

It's also not true that measure(nat) is essentially counting and measure(real) is essentially lebesgue. Types in Hakaru denote measurable spaces, not measures denoted by terms such as counting and lebesgue. It is perfectly possible to express the counting measure over natural numbers as a Hakaru term of type measure(real):

n <~ counting
return nat2real(n)

And it's not the case that the type checker shouldn't be getting to the point of unifying measure(nat) and measure(real). One branch of match x1: ... has the principal type measure(nat) and the other branch has the principal type measure(real), so we need to unify them.

[zaxtax]

Although that is how the typechecker should work. It is definitely not how it does work.

For example, the following program does not typecheck:

match true:
  true: dirac(-3.4)
  false: dirac(1)

[JacquesCarette]

To me, the key part is

• The expressions 37, 42, and match x0: true: 37 false: 42 all have all of the following types: nat, int, real, prob.

with which I agree. The problem is that we don't give them a type that records all of that -- we just "guess" nat and leave it at that. We do patch up a few things via lub, but there is no strong back-patching that occurs to make things really unify.

Wouldn't it be simpler to give things like 37 a "type variable" as type and assert that that variable must unify with the set {nat, int, real, prob}. [which should really be a lattice, not a set]. If we have to force such a variable, we pick the lowest element (if it exists).

That does not give us principal types, but it does give principal typings. Which are usually good enough.

[ccshan]

But we do "give them a type that records all of that". For type inference to return a type is to record that the input term has all the types above that type.

[ccshan]

Sorry, I submitted my comment too soon. I was going to say two more things: First, I like @zaxtax's example. Second, I don't understand @JacquesCarette's comment about principal typings. I understand from https://github.iu.edu/ccshan/ppaml/blob/master/papers/p42-jim.pdf that having principal typings is a stronger property than having principal types, and the difference is about the type environment. In all the examples so far, the type environment is not involved. And if we have principal typings, we certainly have principal types.

We've been managing to avoid unification.

[JacquesCarette]

Looks like this might all be moot - @yuriy0 's been implementing some stuff on the Haskell side which looks like it's going to deal with a lot of this.

[I might have mis-remembered the kinds of typings I had in mind; I was thinking of representing things via (type) constraints rather than type schemes (or environment schemes). It's like in algebra, where 'principal ideals' are great, but not always available; you can, on the other hand, get a Groebner basis for any ideal, which is just as good as having a generator for most of the work needed.]

[yuriy0]

This has been fixed by the various changes to the parser and pretty printer, and by manually fixing programs generated by the old pretty printer.