TL;DR How can I encode static invariants that are possible with GADTs when using a tagless encoding?
I am building a dsl on top of a SQL like language, with the goals of rounding out some of the rough edges, type safety and minor query optimization.
In my first pass I used GADT's to enforce several restrictions that the target language would execute but the output was in most cases garbage. Namely columns of mixed length in select statements like
select mean x, x by date, time from tbl
I prevent these mixed selections by tagging columns as either Selections (vectors) or Reductions (scalars) and thus the compiler can statically prevent these operations. I never did figure out how to prevent selecting from a groupby, however.
The next feature to scratch off is to add type checking to the column arithmetic operations, my first bad idea was to add another phantom type to carry the column type. This wont work as it would break my Schema type and I could no longer select columns of mixed types. This led me to think a tagless embedding of Columns might be appropriate as I could then get the appropriate representation (type, size, etc.) depending on the context. The downside is that this would appear to defer all the invariants I want to encode til run-time. To illustrate this here is rough pseudo code for add in the GADT and tagless approaches.
-- | GADT
add :: Column ty s1 -> Column ty s2
add a b = BinExpr Add a b
-- | Tagless
add :: Column c => c -> c -> c
add a b | (a :: ColType) == (b :: ColType) = binexpr Add a b
| TypeMismatch a b
The GADT approach also has the benefit of being able to specify Num ty => ... to prevent addition on columns of strings. This type of issue would seem to propagate through all my code as I now have to defer to runtime checking to ensure prevention of Selects of mixed size or Group only working on a Query Selection. So my question is: Can I somehow retain the static guarantees of GADTs while using the flexibility of a Tagless style?
My current GADTs
{-# LANGUAGE
GADTs
, DataKinds
, TypeFamilies #-}
-- Kinds
-- | State Tags
-- These constructors are promoted to the kind level to be used as
-- phantom types to enforce static query invariants. For instance
-- these are strategically used to prevent selecting from a Groupby
-- or preventing selection of mixlengthed columns
data Sz = Selection | Reduction deriving Show
--------------------------------------------------------------------
-- Schema
data Schema = Schema {
name :: Maybe String,
spec :: [Column Selection]
} deriving Eq
--------------------------------------------------------------------
-- Column Datatype
data Column (a :: Sz) where
Column :: String -> Column Selection
Assign :: String -> Column a -> Column a
FKey :: String -> Schema -> Column Selection
BinExpr :: BinOp -> Column a -> Column b -> Column (ColOp a b)
LogExpr :: LogOp -> Column a -> Column b -> Column Selection
AggExpr :: AggOp -> Column Selection -> Column Reduction
type family ColOp (a :: Sz) (b :: Sz) where
-- | If both sides a scalar then output
-- is still a scalar, otherwise return
-- a vector, as we can perform the op
-- elemwise or brodcast a scalar across
-- the vector
ColOp Reduction Reduction = Reduction
ColOp a b = Selection
--------------------------------------------------------------------
-- Query types
class Tabular repr where
meta :: repr (a :: Sz) -> Schema
data Query (a :: Sz) where
Table :: Schema -> Query Selection
Select :: (Tabular t, Show (t b)) => [Column a] -> t b -> Query Selection
Where :: (Tabular t, Show (t Selection)) => [Column Selection] -> t Selection -> Query Selection
Group :: (Tabular t, Show (t Selection)) => [Column Selection] -> t Selection -> Query Reduction
Tagless Column Prototype
{-# language FlexibleInstances #-}
data Sz = Selection | Reduction
deriving Show
data ColType
= Int | Float | String | Bool
| TypeMismatch ColType ColType
deriving (Show, Eq)
data BinOp = Add | Mul
data AggOp = Mean | Count
-- Tagless AST
class Show repr => Column repr where
column :: String -> ColType -> repr
assign :: String -> repr -> repr
binExpr :: BinOp -> repr -> repr -> repr
aggExpr :: AggOp -> repr -> repr
-- Show Instances
instance Show BinOp where
show Add = " + "
show Mul = " * "
instance Show AggOp where
show Mean = "mean "
show Count = "count "
-- I Would like to bring these into the type level (ie performed statically)
opSz :: Sz -> Sz -> Sz
opSz Reduction Reduction = Reduction
opSz a b = Selection
typeCheck :: ColType -> ColType -> ColType
typeCheck a b | a == b = a
| otherwise = TypeMismatch a b
-- Tagless Interpreters
-- | Stringify
instance Column ([Char]) where
column s t = s
assign s c = s ++ ": " ++ show c
binExpr o l r = l ++ show o ++ r
aggExpr op l = show op ++ l
-- | Column Size
instance Column Sz where
column s t = Selection
assign s c = c :: Sz
binExpr o l r = opSz l r
aggExpr op l = Reduction
-- | Column Type
instance Column ColType where
column s t = t
assign s c = c :: ColType
binExpr o l r = typeCheck l r
aggExpr o l = l :: ColType
add :: Column c => c -> c -> c
add l r = binExpr Add l r
columns :: Column c => [c]
columns = [ column "a" Float
, column "b" Int
, column "c" String ]
a :: Column c => c
a = columns !! 0
b :: Column c => c
b = columns !! 1
-- add a b :: ColType => TypeMismatch Float Int
Edit: I can get similar behavior by adding a type parameter to the class
class Column repr where
column :: String -> repr Selection
assign :: String -> repr (a :: Sz) -> repr (a :: Sz)
binExpr :: BinOp -> repr (a :: Sz) -> repr (b :: Sz) -> repr (OpSz a b)
aggExpr :: AggOp -> repr Selection -> repr Reduction
But I am still curious how I can define an interpreter of the ast that brings ColType to the type level such that I can define add :: C t -> C t -> C t so add a :: (C String) b :: (C Int) doesn't typecheck