haskellgadtexistential-typedata-kinds

Using GADTs with DataKinds for type level data constructor constraints in functions

I'm trying to use a GADT with DataKinds, as shown below

{-# LANGUAGE KindSignatures, DataKinds, GADTs #-}
module NewGadt where

data ExprType = Var | Nest

data Expr (a :: ExprType) where
  ExprVar :: String -> Expr Var
  ExprNest :: Expr a -> Expr Nest

data BaseExpr
  = BaseExprVar String
  | BaseExprNest BaseExpr

translate :: BaseExpr -> Expr a
translate (BaseExprVar id) = ExprVar id
translate (BaseExprNest expr) = ExprNest $ translate expr

Compile error:

/home/elijah/code/monty/src/NewGadt.hs:15:32: error:
    • Couldn't match type ‘a’ with ‘'Var’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          bexprToExpr :: forall (a :: ExprType). BaseExpr -> Expr a
        at src/NewGadt.hs:14:1-33
      Expected type: Expr a
        Actual type: Expr 'Var
    • In the expression: ExprVar id
      In an equation for ‘bexprToExpr’:
          bexprToExpr (BaseExprVar id) = ExprVar id
    • Relevant bindings include
        bexprToExpr :: BaseExpr -> Expr a (bound at src/NewGadt.hs:15:1)
   |
15 | bexprToExpr (BaseExprVar id) = ExprVar id
   |                                ^^^^^^^^^^

I would like to do this so certain functions can only work on a specific type of expr, for example:

printVariable :: Expr Var -> IO ()
printVariable (ExprVar id) = putStrLn id

printNested :: Expr Nest -> IO ()
printNested (ExprNest inner) = putStrLn "nested expression"

printExpr :: Expr a -> IO ()
printExpr expr@ExprVar {} = printVariable expr
printExpr expr@ExprNest {} = printNested expr

And of course, calling printVariable with an Expr Nest should fail compilation.

Is there a way I can have the translate function return Expr a like this? Or is this an inappropriate usage of DataKinds & GADTs?

Edit:

Solution worked! But, I had to upgrade to ghc >=8.10 and enable StandaloneKindSignatures, PolyKinds

Solution

  • You can define an existential wrapper

    {-# Language PolyKinds                #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications         #-}

import Data.Kind (Type)

--
--   Exists @ExprType :: (ExprType -> Type) -> Type
--
type Exists :: forall k. (k -> Type) -> Type
data Exists f where
  Exists :: f x -> Exists f

    and return Exists Expr

    translate :: BaseExpr -> Exists @ExprType Expr
translate (BaseExprVar id)
  = Exists (ExprVar id)
translate (BaseExprNest expr)
  | Exists a <- translate expr
  = Exists (ExprNest a)

    This uses pattern guards to unpack the existential type

    pattern guards are of the form p <- e, where p is a pattern (see Section 3.17) of type t and e is an expression type t1. They succeed if the expression e matches the pattern p, and introduce the bindings of the pattern to the environment.

    Haskell Report

    and is equivalent to these

    translate (BaseExprNest expr) = case translate expr of
  Exists a -> Exists (ExprNest a)

    {-# Language ViewPatterns #-}

translate (BaseExprNest (translate -> Expr a)) = Exists (ExprNest a)

    But try it with let or where and it won't work.

    References