Re: [stack] Type for row based languages

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