first version of GADTs

lambdacube-dsl/Parser.hs

@@ -182,7 +182,7 @@ moduleDef fname = do
     idefs <- many importDef
     -- TODO: unordered definitions
     defs <- groupDefinitions . concat <$> many (choice
-        [ (:[]) . DDataDef <$> dataDef
+        [ (:[]) <$> dataDef
         , concat <$ keyword "axioms" <*> localIndentation Gt (localAbsoluteIndentation $ many axiom)
         , (:[]) <$> typeSignature
         , const [] <$> typeSynonym
@@ -195,6 +195,7 @@ moduleDef fname = do
         mkDef = \case
             ValueDef d -> [ValueDef $ id *** ($ ps) $ d]
             DDataDef d -> [DDataDef d]
+            GADT a b c -> [GADT a b c]
             InstanceDef c t -> [InstanceDef c t]
             TypeSig d -> [TypeSig d]
             _ -> []
@@ -310,21 +311,38 @@ ty = do
   where
     tArr t a = Ty' (t <-> a) $ TArr_ t a
 
-dataDef :: P DataDefR
+dataDef :: P DefinitionR
 dataDef = do
  keyword "data"
  localIndentation Gt $ do
   tc <- typeConstructor
-  tvs <- many typeVar
+  tvs <- many $ parens ((,) <$> typeVar <* operator "::" <*> ty)
+            <|> (,) <$> typeVar <*> pure (Ty' mempty $ Star_ C)
   let dataConDef = do
-        tc <- typeConstructor
+        tc <- upperCaseIdent
         tys <-   braces (sepBy (FieldTy <$> (Just <$> varId) <*> (keyword "::" *> optional (operator "!") *> typeExp)) comma)
             <|>  many (optional (operator "!") *> (FieldTy Nothing <$> typeAtom))
         return $ ConDef tc tys
-  operator "="
-  ds <- sepBy dataConDef $ operator "|"
-  derivingStm
-  return $ DataDef tc tvs ds
+  do
+    do
+      keyword "where"
+      ds <- localIndentation Ge $ localAbsoluteIndentation $ many $ do
+        c <- do
+            c <- upperCaseIdent
+            localIndentation Gt $ do
+                operator "::"
+            return c
+        localIndentation Gt $ do
+            t <- typeExp
+            return (c, t)
+      return $ GADT tc tvs ds
+   <|>
+    do
+      operator "="
+      ds <- sepBy dataConDef $ operator "|"
+      derivingStm
+      return $ DDataDef $ DataDef tc tvs ds
+
 
 derivingStm = optional $ keyword "deriving" <* (void_ typeConstructor <|> void_ (parens $ sepBy typeConstructor comma))
 

lambdacube-dsl/Type.hs

@@ -395,7 +395,7 @@ data Q a = Q {qualifier :: [String], qData :: a} -- | UQ a
 
 type Prec = Map EName (FixityDir, Int)
 
-data DataDef a = DataDef String [String] [ConDef a]
+data DataDef t = DataDef EName [(TName, t)] [ConDef t]
     deriving (Show)
 data ConDef a = ConDef EName [FieldTy a]
     deriving (Show)
@@ -448,6 +448,7 @@ data Definition t e r
   | ValueDef (Pat r, e)
   | TypeSig (String, t)
   | DDataDef (DataDef t)
+  | GADT EName [(TName, t)] [(EName, t)]
   | InstanceDef Class t
   | DFixity EName (FixityDir, Int)
     deriving Show

lambdacube-dsl/Typecheck.hs

@@ -191,17 +191,34 @@ inference_ penv m = runExcept $ fst <$>
         definitions <- inferDefs definitions
         return Module{..}
 
+trace' s = trace (show s) s
+
 inferDefs :: [Definition TyR (Exp Range) Range] -> TCM [Definition Typing (Exp STyping) STyping]
 inferDefs [] = return []
 inferDefs (ValueDef d: ds) = do
     (d, f) <- inferDef d
     ds <- f $ inferDefs ds
     return (ValueDef d: ds)
-inferDefs (DDataDef d@(DataDef con vars cdefs): ds) = withTyping (uncurry Map.singleton $ tyConKind d) $ do
-    cdefs <- withTyping (Map.fromList [(primed v, [] ==> Star) | v <- vars]) $ mapM inferConDef cdefs
+inferDefs (DDataDef d@(DataDef con vars cdefs): ds) = do
+  vars <- forM vars $ \(n, k) -> do
+    k <- inferKind' k
+    return (n, k)
+  withTyping (uncurry Map.singleton $ tyConKind con vars) $ do
+    cdefs <- withTyping (Map.fromList [(primed v, k) | (v, k) <- vars]) $ mapM inferConDef cdefs
     let d' = DataDef con vars cdefs
     ds <- withTyping (Map.fromList $ tyConTypes d') $ inferDefs $ selectorDefs d ++ ds
     return (DDataDef d': ds)
+inferDefs (GADT con vars cdefs: ds) = do
+  vars <- forM vars $ \(n, k) -> do
+    k <- inferKind' k
+    return (n, k)
+  withTyping (uncurry Map.singleton $ tyConKind con vars) $ do
+    cdefs <- forM cdefs $ \(c, t) -> do
+        t <- inferKind' t
+        return (c, t)
+    let d' = GADT con vars cdefs
+    ds <- withTyping (Map.fromList cdefs) $ inferDefs ds
+    return (d': ds)
 inferDefs (TypeSig (n, a): ds) = do
     a' <- inferKind' a
     let (n', a'') = mangleAx . (id *** generalizeTypeVars) $ (n, a')
@@ -238,7 +255,7 @@ replCallType n nt = \case
 modTag f (Exp t x) = Exp (f t) x
 
 selectorDefs :: DataDef (Ty' Range) -> [Definition TyR (Exp Range) Range]
-selectorDefs d@(DataDef n vs cs) =
+selectorDefs d@(DataDef n _ cs) =
     [ ValueDef
       ( PVar mempty sel
       , ELam mempty
@@ -253,27 +270,27 @@ selectorDefs d@(DataDef n vs cs) =
     ]
 
 selectorTypes :: DataDef Typing -> [(EName, Typing)]
-selectorTypes d@(DataDef n vs cs) =
+selectorTypes d@(DataDef n _ cs) =
     [ (sel, generalizeTypeVars $ tyConResTy d .~> t)
     | ConDef cn tys <- cs
     , FieldTy (Just sel) t <- tys
     ]
 
-tyConResTy :: DataDef a -> Typing
+tyConResTy :: DataDef Typing -> Typing
 tyConResTy (DataDef n vs _)
-    = [] ==> foldl app (Ty_ k $ TCon_ n) (zip [i-1,i-2..] $ map (Ty_ Star . TVar_) vs)
+    = [] ==> foldl app (Ty_ k $ TCon_ n) (zip [i-1,i-2..] [TVar (typingToTy k) n | (n, k) <- vs])
   where
     app x (i, y) = TApp (StarToStar i) x y
     k = StarToStar i
     i = length vs
 
 tyConTypes :: DataDef Typing -> [(EName, Typing)]
-tyConTypes d@(DataDef n vs cs) =
+tyConTypes d@(DataDef n _ cs) =
     [ (cn, foldr (.~>) (tyConResTy d) $ map fieldType tys)
     | ConDef cn tys <- cs
     ]
 
-tyConKind (DataDef n vs _) = (primed n, [] ==> StarToStar (length vs))
+tyConKind n vs = (primed n, foldr (.~>) ([] ==> Star) $ map snd vs)
 
 exportEnv :: ModuleT -> PolyEnv
 exportEnv Module{..}
@@ -285,7 +302,8 @@ exportEnv Module{..}
 
 axs = \case
     ValueDef (PVar _ n, e) -> [(n, snd $ getTag e)]
-    DDataDef d -> tyConKind d: tyConTypes d ++ selectorTypes d
+    DDataDef d@(DataDef n vs _) -> tyConKind n vs: tyConTypes d ++ selectorTypes d
+    GADT n vs defs -> tyConKind n vs: defs
     TypeSig x -> [x]
     _ -> []
 

lambdacube-dsl/tests/accept/Prelude.lc

@@ -43,18 +43,14 @@ data Maybe a
 
 ---------------------------------------
 
-axioms
-
-  Nat :: *
-
-axioms
-
-  Char, String, Word, Int, Float :: *
-
-axioms
-
-  Vec :: Nat -> * -> *
-
+data Nat where
+data Char where
+data String where
+data Word where
+data Int where
+data Float where
+
+data Vec (n :: Nat) a where
   V2 :: Component a => a -> a -> Vec 2 a
   V3 :: Component a => a -> a -> a -> Vec 3 a
   V4 :: Component a => a -> a -> a -> a -> Vec 4 a
@@ -72,10 +68,7 @@ axioms
   V3F :: Float -> Float -> Float -> Vec 3 Float
   V4F :: Float -> Float -> Float -> Float -> Vec 4 Float
 
-axioms
-
-  Mat :: Nat -> Nat -> * -> *
-
+data Mat (i :: Nat) (j :: Nat) a where
   M22F :: Vec 2 Float -> Vec 2 Float -> Mat 2 2 Float
   M23F :: Vec 2 Float -> Vec 2 Float -> Vec 2 Float -> Mat 2 3 Float
   M24F :: Vec 2 Float -> Vec 2 Float -> Vec 2 Float -> Vec 2 Float -> Mat 2 4 Float
@@ -239,25 +232,31 @@ data PointSpriteCoordOrigin
     | UpperLeft
 
 
-axioms
+data Depth a where
+data Stencil a where
+data Color a where
 
-  Depth, Stencil, Color :: * -> *
-  Triangle, Line, Point, TriangleAdjacency, LineAdjacency :: *
+data Triangle where
+data Line where
+data Point where
+data TriangleAdjacency where
+data LineAdjacency where
+
+axioms
 
 {- TODO: more precise kinds
   FetchPrimitive       :: PrimitiveType -> *
   FragmentOperation    :: Semantic -> *
   FragmentOut          :: Semantic -> *
-  Image                :: Nat -> Semantic -> *
   RasterContext        :: PrimitiveType -> *
   VertexOut            :: ???
   VertexStream         :: PrimitiveType -> * -> *
 -}
   Output :: *
-  AccumulationContext, Blending, FetchPrimitive, FragmentFilter, FragmentOperation, FragmentOut, Input, Interpolated, RasterContext, VertexOut :: * -> *
+  AccumulationContext, Blending, FragmentFilter, FragmentOperation, FragmentOut, Input, Interpolated, VertexOut :: * -> *
   VertexStream :: * -> * -> *
   PrimitiveStream :: * -> Nat -> * -> *
-  Image, FragmentStream, FrameBuffer :: Nat -> * -> *
+  FragmentStream, FrameBuffer :: Nat -> * -> *
 
   -- TODO: eliminate
   fromInt :: Num a => Int -> a
@@ -305,28 +304,33 @@ axioms
 
   VertexOut           :: (t ~ FTRepr' a) => Vec 4 Float -> Float -> (){-TODO-} -> a -> VertexOut t
 
-  -- GADT RasterContext
+data RasterContext a where
   TriangleCtx         :: CullMode -> PolygonMode -> PolygonOffset -> ProvokingVertex -> RasterContext Triangle
-  PointCtx            :: PointSize -> Float -> PointSpriteCoordOrigin                 -> RasterContext Point
-  LineCtx             :: Float -> ProvokingVertex                                      -> RasterContext Line
+  PointCtx            :: PointSize -> Float -> PointSpriteCoordOrigin                -> RasterContext Point
+  LineCtx             :: Float -> ProvokingVertex                                    -> RasterContext Line
 
-  -- GADT FetchPrimitive
-  Points              :: FetchPrimitive Point
-  Lines               :: FetchPrimitive Line
-  Triangles           :: FetchPrimitive Triangle
-  LinesAdjacency      :: FetchPrimitive LineAdjacency
-  TrianglesAdjacency  :: FetchPrimitive TriangleAdjacency
+data FetchPrimitive a where
+   Points              :: FetchPrimitive Point
+   Lines               :: FetchPrimitive Line
+   Triangles           :: FetchPrimitive Triangle
+   LinesAdjacency      :: FetchPrimitive LineAdjacency
+   TrianglesAdjacency  :: FetchPrimitive TriangleAdjacency
+
+axioms
 
   AccumulationContext :: (t' ~ FragOps t) => t -> AccumulationContext t'
 
-  ColorImage          :: (Num t, color ~ VecScalar d t) => forall (a :: Nat) . color
-                                -> Image a (Color color)
+data Image (a :: Nat) b{-Semantic-} where
+  ColorImage          :: (Num t, color ~ VecScalar d t)
+                      => forall (a :: Nat) . color  -> Image a (Color color)
   DepthImage          :: forall (a :: Nat) . Float  -> Image a (Depth Float)
   StencilImage        :: forall (a :: Nat) . Int    -> Image a (Stencil Int)
 
+axioms
+
   Smooth, NoPerspective
-                        :: (Floating t) => t -> Interpolated t
-  Flat              ::                       t -> Interpolated t
+                      :: (Floating t) => t -> Interpolated t
+  Flat                ::                 t -> Interpolated t
 
   ColorOp             :: (mask ~ VecScalar d Bool, color ~ VecScalar d c, Num c) => Blending c -> mask
                                                             -> FragmentOperation (Color color)