Problem with frege.java.Util.Properties

[ForNeVeR]

Some methods of Properties type seems to be incorrectly typed. For example, consider load method:

data Properties = native java.util.Properties where
  ...
  native load :: MutableIO Properties -> MutableIO Reader -> IO () throws IOException
               | MutableIO Properties -> MutableIO InputStream -> IO () throws IOException

It accepts only MutableIO InputStream but the language doesn't provide an ability to get MutableIO InputStream at all.

The same seems to be case with almost all methods of Properties type. I've discussed it with @Ingo60 in IRC and he thinks it may be caused due to problem with frege-native-gen (I'll check it eventually), so we maybe should rise another issue there.

The solution may be to simply remove MutableIO from InputStream (and maybe some another types) in method signatures of Properties. If the Util class was auto-generated and meant to be changed only by regeneration - we should fix the frege-native-gen first.

I am ready to provide some code samples about which I think they should compile and they are currently not.

[mmhelloworld]

Isn't InputStream substitutable for MutableIO Inputstream as it is a mutable native type?

On Monday, March 16, 2015, Friedrich von Never notifications@github.com wrote:

Some methods of Properties type seems to be incorrectly typed. For example, consider load method:

data Properties = native java.util.Properties where ... native load :: MutableIO Properties -> MutableIO Reader -> IO () throws IOException | MutableIO Properties -> MutableIO InputStream -> IO () throws IOException

It accepts only MutableIO InputStream but the language doesn't provide an ability to get MutableIO InputStream at all.

The same seems to be case with almost all methods of Properties type. I've discussed it with @Ingo60 https://github.com/Ingo60 in IRC and he thinks it may be caused due to problem with frege-native-gen (I'll check it eventually), so we maybe should rise another issue there.

The solution may be to simply remove MutableIO from InputStream (and maybe some another types) in method signatures of Properties. If the Util class was auto-generated and meant to be changed only by regeneration - we should fix the frege-native-gen first.

I am ready to provide some code samples about which I think they should compile and they are currently not.

— Reply to this email directly or view it on GitHub https://github.com/Frege/frege/issues/129.

[ForNeVeR]

As i can see - no, it don't. Citing the documentation (see 8.6.3 of the Language Reference):

A native type M whose values would, by the rules above, appear everywhere with type Mutable RealWorld M, is called a mutable only type. It can be declared like

data M = mutable native ...

and can appear in type signatures as just M. The compiler will then apply the rules above as if the type was Mutable RealWorld M, [...]

So it is not a MutableIO (remember that MutableIO = Mutable RealWorld), it is simply treated as MutableIO in any native declarations. So there is no need to explicitly declare it as MutableIO in the declaration of frege.java.util.Properties or any other native declarations.

Please feel free to correct me if I'm wrong. I am still learning Frege and can mistake.

[Ingo60]

No, it isn't. Since a type constructor can never unify with a type application. I suggest editing Util.fr with find/replace for the critical types.

[mmhelloworld]

I think I just read this The compiler will then apply the rules above as if the type was Mutable RealWorld M and misunderstood.

Now it is clear from this statement from language reference The type checker expects a Mutable s m, but the 'as if' above concerns only sanity checks for types of native functions, the normal typing rules will never actually unify Mutable s m with M .

I will send a pull request later today to fix this.

[Ingo60]

I shall also let the compiler emit a warning when it sees such "impossible" types, for easier diagnosis.

[mmhelloworld]

That would be better! Thanks!

Here is the pull request to fix Util.fr: https://github.com/Frege/frege/pull/130

[Ingo60]

Reopened to keep track of compiler changes.

[Ingo60]

Fixed with commit 31d2574d471f1754fd88353f0c1eac2e92d315c0

If a type is mutable only, it must not appear wrapped in Mutable.