Type for row based languages

[hallucious]

I think that functions on rows can be given types using type constraints - even the weird ones like bi@.
A type can be given to the composition of functions f g h that is equivalent whether f g or g h are taken first.

Let f : ( A -> B ) where P
Let g : ( C -> D ) where Q
In a type system that does not have ad-hoc polymorphism, then
  f g : ( A -> D ) where P and Q and B = C
For example:
bi@ : ( A B (B -> C d) -> E C d d) where A C = E B

And in a type system that does have it,
 then  f g : ( A -> D ) where P and Q and B < C

I wrote more details about such a system at
http://www.nothingontelly.com/RowTypes.txt

Is there pre-existing work on this?
Have I made a mistake? Missed something?
Is there a book I should have read?

[John Nowak]

On Apr 4, 2009, at 5:27 PM, hallucious wrote:

> Is there pre-existing work on this?

Nothing published that I'm aware of, no. Existing work on type systems  
for concatenative languages (and there isn't much) has mostly focused  
on systems with decidable type inference.

> Have I made a mistake? Missed something?

Not that i can see. Do you have any application in mind for it?

I suppose my only comment is that I'm not sure if your approach is  
ideal for concatenative languages. In my personal experience,  
intersection types seem to be a much better match. For example, the  
type of 'dup apply' in a system with intersection types can be stated  
rather simply:

     A (b /\ (A b -> C)) -> C

If you assume 'dup' to have the type 'A (b /\ c) -> A b c', inference  
is straightforward:

     A (b /\ c) -> A b c
                   D   (D -> E) -> E

     A (b /\ (D -> E)) -> A b (D -> E)
                          D   (D -> E) -> E

     A (b /\ (A b -> E)) -> A b (D -> E)
                            A b (D -> E) -> E

     A (b /\ (A b -> E)) -> E

As for your '[id] dup' example:

     A -> A (B -> B)
          C (d /\ e) -> C d e

     -- B free in B -> B, make fresh
     A -> A ((B -> B) , (F -> F))
          C (d        , e       ) -> C d e

     A -> A ((B -> B) , (F -> F))
          C ((B -> B) , e       ) -> C (B -> B) e

     A -> A ((B -> B) , (F -> F))
          C ((B -> B) , (F -> F)) -> C (B -> B) (F -> F)

     A -> A ((B -> B) , (F -> F))
          A ((B -> B) , (F -> F)) -> A (B -> B) (F -> F)

     A -> A (B -> B) (F -> F)

Apologies for not having anything more constructive for your system in  
particular.

- John

[John Nowak]

One more thing I should've mentioned. You state that your type system  
is compositional. I should note that you can get this quite easy by  
extending HM with row types and omitting any equivalent to let  
polymorphism. For example, 'dup apply' would fail to type:

     A b -> A b b
            C   (C -> D) -> D

     A (C -> D) -> A (C -> D) (C -> D)
                   C          (C -> D) -> D

     -- error: C occurs in A (C -> D)

Luckily (for some definition of "luck"), something like '[id] dup  
apply' would fail as well:

     A -> A (B -> B)
          C d        -> C d d

     A -> A (B -> B)
          C (B -> B) -> C (B -> B) (B -> B)

     A -> A (B -> B)
          A (B -> B) -> A (B -> B) (B -> B)

     A -> A (B -> B) (B -> B)

     A -> A (B -> B) (B -> B)
          C          (C -> D) -> D

     A -> A (D -> D) (D -> D)
          C          (C -> D) -> D

     A -> A (C -> C) (C -> C)
          C          (C -> C) -> C

     -- error: C occurs in A (C -> C)

For all expressions that do yield valid types, the order in which you  
infer the type does not matter.

Apologies if I'm stating the obvious.

- John

[hallucious]

One motivation for this work was to broaden the range of functions which can be investigated by looking at their type, which can be useful to see their effect. Another was to allow the programmer to provide additional constraints. I also hoped that the type would form a basis for proving properties of any function, using denotation provided by the programmer. I did not want the type system to restrict which functions or algorithms could be considered. We should be free to get a function working empirically, then prove its correctness.

And another was to use inheritance polymorphism, mix in native objects from Java or C# and type their interfaces, and investigate uniqueness types in concatenative languages. Perhaps an undecidable type system is not really necessary for this. But I wanted a type system for experimental programs that might be rejected by conventional type systems.

I do not expect that there is any automated (unguided) procedure to check, for instance, whether two type formulas are equivalent in this system. (Is this what decidable type inference means?)

[hallucious]

One motivation for this work was to broaden the range of functions
which can be investigated by looking at their type, which can be
useful to see their effect. Another was to allow the programmer to
provide additional constraints. I also hoped that the type would form
a basis for proving properties of any function, using denotation
provided by the programmer. I did not want the type system to restrict
which functions or algorithms could be considered. We should be free
to get a function working empirically, then prove its correctness.

And another was to use inheritance polymorphism, mix in native objects
from Java or C# and type their interfaces, and investigate uniqueness
types in concatenative languages. Perhaps an undecidable type system
is not really necessary for this. But I wanted a type system for
experimental programs that might be rejected by conventional type
systems.

I do not expect that there is any automated (unguided) procedure to
check, for instance, whether two type formulas are equivalent in this
system. Is this what decidable type inference means?

[hallucious]

If decidable type inference means that the type of quotations and compositions of functions can be inferred and expressed, then I think that type inference is decidable in this system. You are not forced to simplify. (I should have pointed that out.)

But I do not think that type checking or type equality are decidable.

[John Nowak]

On Apr 4, 2009, at 9:01 PM, hallucious wrote:

> One motivation for this work was to broaden the range of functions  
> which can be investigated by looking at their type, which can be  
> useful to see their effect.

You may want to look at Djinn if you haven't already:
http://lambda-the-ultimate.org/node/1178

> Another was to allow the programmer to provide additional  
> constraints. I also hoped that the type would form a basis for  
> proving properties of any function, using denotation provided by the  
> programmer.

In my opinion, it would be more useful to add types dependent on  
values rather than (or in addition to) higher rank polymorphism and  
subtyping if your goal to allow programmers to prove things. There  
are, as you probably know, a large number of languages that already  
take this approach (Agda, Coq, Epigram, Dependent ML, ATS, etc).

> I do not expect that there is any automated (unguided) procedure to  
> check, for instance, whether two type formulas are equivalent in  
> this system. (Is this what decidable type inference means?)

In practice, I believe undecidable just means "not guaranteed to  
terminate". For example, type inference is undecidable in a language  
like Agda because certain programs will cause the type checking stage  
to never finish.

- John

[John Nowak]

On Apr 4, 2009, at 9:41 PM, hallucious wrote:

> If decidable type inference means that the type of quotations and  
> compositions of functions can be inferred and expressed, then I  
> think that type inference is decidable in this system. You are not  
> forced to simplify. (I should have pointed that out.)

It's easy to infer the constraints, but type inference (I believe)  
also entails checking that those constraints are satisfied and not in  
contradiction to one another. For example, you may have the following  
composition:

     A b -> A b      b Int
            C String d d   -> E

And you could assign it the following type:

     A b -> E where A < C and b = String and b < d and d = Int

This alone is not useful because the type inferred is not valid.

- John

[hallucious]

Hi John,

Thanks for the info and for bearing with me.
I do want to move on to type systems that are useful for compilers.

I shall clarify the subordinate role of this type system in the report.

Adrian

[John Nowak]

On Apr 5, 2009, at 5:09 AM, hallucious wrote:

> Thanks for the info and for bearing with me.
> I do want to move on to type systems that are useful for compilers.

It seems to me that some of the most interesting work in this field  
(type systems for compilers) is being done by the Church Project (http://www.church-project.org 
). They've already done much work on compositional analysis which may  
be useful to you if you're not already familiar with it.

- John