I don't know how to express it. You need to have some dynamic
representation since
dag is a container of `(Int, f Int)`. I've tried to go along this road
type Exp a = Fix (E a)
data E c :: * -> * where
Lit :: Show a => a -> E a c
Op :: Op a -> E a c
App :: Phantom (a -> b) c -> Phantom a c -> E b c
data Op :: * -> * where
Add :: Num a => Op (a -> a -> a)
Mul :: Num a => Op (a -> a -> a)
Neg :: Num a => Op (a -> a)
newtype Phantom a b = Phantom { unPhantom :: b }
But got stuck with the definition of
app :: Exp (a -> b) -> Exp a -> Exp b
app f a = Fix $ App (Phantom f) (Phantom a)
App requires the arguments to be of the same type (in the second type
argument `c`).
2013/2/23 Conal Elliott
On Tue, Feb 19, 2013 at 9:28 PM, Anton Kholomiov < anton.kholomiov@gmail.com> wrote:
Do you think the approach can be extended for non-regular (nested)
algebraic types (where the recursive data type is sometimes at a different type instance)? For instance, it's very handy to use GADTs to capture embedded language types in host language (Haskell) types, which leads to non-regularity.
I'm not sure I understand the case you are talking about. Can you write a simple example of the types like this?
Here's an example of a type-embedded DSEL, represented as a GADT:
data E :: * -> * where Lit :: Show a => a -> E a Op :: Op a -> E a App :: E (a -> b) -> E a -> E b ...
data Op :: * -> * where Add :: Num a => E (a -> a -> a) Mul :: Num a => E (a -> a -> a) Neg :: Num a => E (a -> a) ...
-- Conal