Re: [stack] typing higher-order concatenative languages with standard hindley-milner

On May 31, 2008, at 2:41 AM, Daniel Ehrenberg wrote:

> Can this work for things that use the data stack with a statically
> unknown depth? For example if factorial is defined like
>
> : factorial ( n -- n! )
>    dup zero? [ drop 1 ] [ dup 1 - factorial * ] if ;
>
> it seems like it should be impossible for Haskell to come up with a  
> type for it.

You'd be right it seems!

     (#) = flip (.)
     push a s = (s, a)

     ...

     dup :: (s, a) -> ((s, a), a)
     dup (s, a) = ((s, a), a)

     zerop :: Num a => (s, a) -> (s, Bool)
     zerop (s, a) = (s, a == 0)

     pop :: (s, a) -> s
     pop (s, a) = s

     mul :: Num a => ((s, a), a) -> (s, a)
     mul ((s, a), b) = (s, a * b)

     sub :: Num a => ((s, a), a) -> (s, a)
     sub ((s, a), b) = (s, a - b)

     ifte :: (((s, Bool), s -> s1), s -> s1) -> s1
     ifte (((s, True),  f), _) = f s
     ifte (((s, False), _), g) = g s

     ...

     factorial = dup # zerop # (push (pop # push 1)) #
       (push (dup # push 1 # sub # factorial # mul)) # ifte

     Occurs check: cannot construct the infinite type: s = (s, a)
       Expected type: ((s, a), a) -> ((s, a1), a1)
       Inferred type: (s, a) -> (s, a1)

I should note that Cat cannot handle the definition of 'fact' either,  
incorrectly giving it the type 'A any -> A any'. Recursive definitions  
in a concatenative language are tricky. Fifth can however, so it  
doesn't appear to be anything fundamentally problematic. It may,  
however, be an example of where row variables are needed.

- John