Row polymorphism in Haskell: trouble writing Forth DSL with "transformations"

Question

I've been inspired by the recent Haskell blog activity¹ to try my hand at writing a Forth-like DSL in Haskell. The approach I have taken is simultaneously straightforward and confusing:

{-# LANGUAGE TypeOperators, RankNTypes, ImpredicativeTypes #-}

-- a :~> b represents a "stack transformation"
--          from stack type "a" to stack type "b"
-- a :> b represents a "stack" where the top element is of type "b"
--          and the "rest" of the stack has type "a"
type s :~> s' = forall r. s -> (s' -> r) -> r
data a :> b = a :> b deriving Show
infixl 4 :>

For doing simple things, this works quite nicely:

start :: (() -> r) -> r
start f = f ()

end :: (() :> a) -> a
end (() :> a) = a

stack x f = f x
runF s = s end
_1 = liftS0 1
neg = liftS1 negate
add = liftS2 (+)

-- aka "push"
liftS0 :: a -> (s :~> (s :> a))
liftS0 a s = stack $ s :> a

liftS1 :: (a -> b) -> ((s :> a) :~> (s :> b))
liftS1 f (s :> a) = stack $ s :> f a

liftS2 :: (a -> b -> c) -> ((s :> a :> b) :~> (s :> c))
liftS2 f (s :> a :> b) = stack $ s :> f a b

Simple functions can trivially be transformed into their corresponding stack transformations. Some playing around yields pleasant results so far:

ghci> runF $ start _1 _1 neg add
0

The trouble comes when I try to extend this with higher-order functions.

-- this requires ImpredicativeTypes...not really sure what that means
-- also this implementation seems way too simple to be correct
-- though it does typecheck. I arrived at this after pouring over types
-- and finally eta-reducing the (s' -> r) function argument out of the equation
-- call (a :> f) h = f a h
call :: (s :> (s :~> s')) :~> s'
call (a :> f) = f a

call is supposed to transform a stack of the form (s :> (s :~> s')) to the form s, by essentially "applying" the transformation (held at the tip of the stack) to the "rest" of it. I imagine it should work like this:

ghci> runF $ start _1 (liftS0 neg) call
-1

But in actuality, it gives me a huge type mismatch error. What am I doing wrong? Can the "stack transformation" representation sufficiently handle higher-order functions, or do I need to adjust it?

¹N.B. Unlike how these guys did it, instead of start push 1 push 2 add end, I want it to be runF $ start (push 1) (push 2) add, the idea being that maybe later I can work some typeclass magic to make the push implicit for certain literals.

• https://github.com/leonidas/codeblog/blob/master/2012/2012-02-17-concatenative-haskell.md
• https://gist.github.com/1847747

Petticoat

actually, I'd like to get rid of start too, and just have runF $ _1 _1 add, though I don't really see how that's possible with this setup. – Petticoat

Impredicate types are a generalization of Rank-n types, which allow a forall inside any type constructor, not just function types. – Glockenspiel

Answer 1

Your :~> type is not what you actually want (hence the ImpredicativeTypes). If you just remove type annotation from call then your last sample will work as expected. Another way to make it work is to use less fancy but more appropriate type with extra parameter:

type Tran s s' r = s -> (s' -> r) -> r

call :: Tran (s :> (Tran s s' r)) s' r
call (a :> f) = f a

But if what you are after is a nice DSL syntax and you are can tolerate OverlappingInstances then you can even pretty much get rid of liftSx functions:

{-# LANGUAGE TypeOperators, MultiParamTypeClasses, TypeFamilies,
             FlexibleInstances, FlexibleContexts,
             UndecidableInstances, IncoherentInstances  #-}

data a :> b = a :> b deriving Show
infixl 4 :>


class Stackable s o r where
    eval :: s -> o -> r


data End = End

instance (r1 ~ s) => Stackable s End r1 where
    eval s End = s


instance (Stackable (s :> a) o r0, r ~ (o -> r0)) => Stackable s a r where
    eval s a = eval (s :> a)

instance (a ~ b, Stackable s c r0, r ~ r0) => Stackable (s :> a) (b -> c) r where
    eval (s :> a) f = eval s (f a)

-- Wrap in Box a function which should be just placed on stack without immediate application
data Box a = Box a

instance (Stackable (s :> a) o r0, r ~ (o -> r0)) => Stackable s (Box a) r where
    eval s (Box a) = eval (s :> a)


runS :: (Stackable () a r) => a -> r
runS a = eval () a

-- tests
t1 = runS 1 negate End
t2 = runS 2 1 negate (+) End

t3 = runS 1 (Box negate) ($) End
t4 = runS [1..5] 0 (Box (+)) foldr End
t5 = runS not True (flip ($)) End

t6 = runS 1 (+) 2 (flip ($)) End

Tommie

Answer 2

The problem is that your type synonym is a polymorphic type

type s :~> s' = forall r. s -> (s' -> r) -> r

Using a polymorphic type as an argument to a type constructor other than -> is called "impredicativity". For instance, the following would be an impredicative use

Maybe (forall a. a -> a)

For various reasons, type inference with impredicativity is hard, that's why GHC complains. (The name "impredicative" comes from logic and the Curry-Howards isomorphism.)

In your case, the solution is simply to use an algebraic data type with a constructor:

data s :~> s' = StackArr { runStackArr :: forall r. s -> (s' -> r) -> r}

Basically, the explicit constructor StackArr supplies enough hints to the type checker.

Alternatively, you can try the ImpredicativeTypes language extension.

Rushy

The problem with using a data declaration is that it pollutes the desired syntax. The reason the type synonym works nicely is because the transformation is a function, and these functions can be chained together by function application as if it were function composition. I did try ImpredicativeTypes, which allows the call to be well-typed, but using call as desired is impossible; there's something inherently wrong with the type I gave it. I think the problem is that the typechecker can't understand the "function application" going on at the type level. – Petticoat