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

The type of factorial in Cat is correct.
Most mathematical operators return "any", because they are not bound
to specific types.
For example "mul" has type "(any any -> any)" whereas "mul_int" has
type "(int int -> int)".


On Sat, May 31, 2008 at 3:14 AM, John Nowak <[email protected]> wrote:
>
> 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
>
>