Re: [stack] Notation for typed arrays in Cat

On Apr 4, 2008, at 7:53 PM, John Nowak wrote:

>    -- concatenative?
>    swap   :: [A b c] [A c b] 'fn
>    i      :: [A [A] [B] 'fn] [B] 'fn
>    unlist :: [A b 'list [A] [C] 'fn [A b b list] [C] 'fn] [C] 'fn

Here's another attempt at a concatenative type notation. We assume  
some function 'r' that pushes a fresh row variable onto the stack and  
some function 's' that pushes a fresh scalar variable onto the stack.  
You can then use *any normal function* to manipulate these on the type  
level where computation is done using the *types* of those normal  
functions. We also have some binary function 'fn' for making functions  
where the second argument describes how to *change* the first, some  
unary function 'list' for making a parameterized list, and a nullary  
function 'num' for making a number. Oh, and a 'prod' function that  
returns the type of the production of a function. And I use my tick  
notation as well as otherwise you need 'swap' to define the type of  
'swap', etc...

Now that I've totally confused you, here you go:

    swap :: [r s s]        [`ba]       fn
    dup  :: [r s]          [`aa]       fn
    drop :: [r s]          [`b]        fn
    nip  :: [r s s]        [swap drop] fn
    add  :: [r num num]    [drop]      fn
    cons :: [r s dup list] [nip]       fn

And now a bit more complicated:

    i    :: [v dup quote [drop v] fn] [nip prod] fn

Here's a trace of 'i' to see how it might be working:

    v:        A
    dup:      A A
    quote:    A [A]
    [drop v]: A [A] [drop B]
    fn:       A [A] [A drop B]
              A [A] [B]
              A [A -> B]
    - - -
    nip:      [A -> B]
    prod:     B


This is obviously very, very loose. It seems you'd really need more  
appropriate type-level combinators. Then there's the whole issue of  
giving back coherent concatenative types after performing inference...

To be clear, this is not a serious proposal. If anyone thinks there's  
a shred of feasibility however, I'd be interested to hear about it...

- John