A series of polymorphisms in Haskell: the problem of writing Forth DSL with "conversions"

Question

I was inspired by the recent activities of the Haskell ¹ blog to try my hand at writing Forth-like DSL in Haskell. The approach that I took is both simple 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 simple things, this works pretty well:

 start :: (() -> r) -> r start f = f () end :: (() :> a) -> a end (() :> a) = a stack xf = fx runF s = s end _1 = liftS0 1 neg = liftS1 negate add = liftS2 (+) -- aka "push" liftS0 :: a -> (s :~> (s :> a)) liftS0 as = stack $ s :> a liftS1 :: (a -> b) -> ((s :> a) :~> (s :> b)) liftS1 f (s :> a) = stack $ s :> fa liftS2 :: (a -> b -> c) -> ((s :> a :> b) :~> (s :> c)) liftS2 f (s :> a :> b) = stack $ s :> fab 

Simple functions can be trivially converted to corresponding stack transformations. Some game around gives nice results so far:

 ghci> runF $ start _1 _1 neg add 0 

The problem arises when I try to extend it 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 = fah call :: (s :> (s :~> s')) :~> s' call (a :> f) = fa 

call should convert the form stack (s :> (s :~> s')) to form s , essentially "applying" the transformation (held on top of the stack) to "rest" it. I believe that should work as follows:

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

But actually it gives me a huge type mismatch error. What am I doing wrong? Can the stack transform view handle higher-order functions, or do I need to adjust it?

¹ NB Unlike the way 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 is that maybe later I can work with a mask of type typeclass to make push implicit for certain literals.

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

Answer 1

Type :~> not the one you actually want (hence ImpredicativeTypes ). If you simply remove the type annotation from call , then your last sample will work as expected. Another way to make it work is to use a less fantastic, but more appropriate type with an additional parameter:

 type Tran ss' r = s -> (s' -> r) -> r call :: Tran (s :> (Tran ss' r)) s' r call (a :> f) = fa 

But if what you need is a good DSL syntax, and you can tolerate OverlappingInstances , then you can even get rid of the liftSx functions pretty much:

 {-# LANGUAGE TypeOperators, MultiParamTypeClasses, TypeFamilies, FlexibleInstances, FlexibleContexts, UndecidableInstances, IncoherentInstances #-} data a :> b = a :> b deriving Show infixl 4 :> class Stackable sor 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 sar where eval sa = eval (s :> a) instance (a ~ b, Stackable sc r0, r ~ r0) => Stackable (s :> a) (b -> c) r where eval (s :> a) f = eval s (fa) -- 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 () ar) => 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 

Answer 2

The problem is that the synonym of your type is a polymorphic type

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

Using a polymorphic type as an argument to a constructor of a type other than -> is called impermeability. For example, the following would be inappropriate use

 Maybe (forall a. a -> a) 

For various reasons, the type of output with consistency is difficult, so the GHC complains. (The name "impredicative" comes from the logic and isomorphism of Curry-Howards.)

In your case, the solution simply uses the type of algebraic data with the constructor:

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

Basically, the explicit StackArr constructor provides enough hints for type checking.

Alternatively, you can try the ImpredicativeTypes language ImpredicativeTypes .