haskellpolymorphismhigher-order-functionsconcatenative-languageimpredicativetypes

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


I've been inspired by the recent Haskell blog activity1 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?

1N.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.


Solution

  • 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