Add typeable (#208)

amuletml.cabal

@@ -255,6 +255,7 @@ library
                      , Types.Infer.Pattern
                      , Types.Infer.Function
                      , Types.Unify.Equality
+                     , Types.Derive.Typeable
                      , Types.Infer.Constructor
                      -- Pretty
                      , Text.Dot

lib/amulet/option.ml

@@ -2,6 +2,8 @@ open import "./base.ml"
 
 type option 'a = Some of 'a | None
 
+deriving typeable option
+
 let from_option x = function
   | Some x -> x
   | None -> x

lib/amulet/typeable.ml

@@ -0,0 +1,35 @@
+open import "./base.ml"
+open import "./option.ml"
+
+type 'a :~: 'b =
+  Refl : 'a ~ 'b => 'a :~: 'b
+
+deriving typeable (:~:)
+
+type proxy 'a = Proxy
+
+deriving typeable proxy
+
+let is_same_type (p : proxy 'a) (q : proxy 'b) : option ('a :~: 'b) =
+  eq_type_rep (type_of p) (type_of q)
+    (fun _ -> Some (Refl : 'a :~: 'b))
+    (fun _ -> None)
+
+let cast
+  :
+    forall 'a 'b. typeable 'a * typeable 'b => 'a -> option 'b
+  =
+    fun x ->
+      eq_type_rep
+        (type_of (Proxy @'a))
+        (type_of (Proxy @'b))
+        (fun _ -> Some x)
+        (fun _ -> None)
+
+(** An opaque box that carries typeable evidence *)
+type dynamic =
+  Dynamic : forall 'a. typeable 'a => 'a -> dynamic
+
+deriving typeable dynamic
+
+let from_dynamic (Dynamic x) = cast x

lib/prelude.ml

@@ -1,13 +1,13 @@
 include import "./amulet/base.ml"
 include import "./amulet/option.ml"
 include import "./amulet/list.ml"
+include import "./amulet/typeable.ml"
 
 include import "./data/foldable.ml"
 include import "./data/traversable.ml"
 
 include import "./data/enumeration.ml"
 
-
 external private val prim_parse_int : (int -> option int) -> option int -> string -> option int =
   "function(Some, None, x) \
      if tonumber(x) and ((math.modf(tonumber(x))) == tonumber(x)) then \

src/Backend/Lua/Builtin.hs

@@ -216,4 +216,47 @@ builtins =
         end
       |] )
 
+  , ( tcTYPEABLE, "_Typeable", [], Just (1, \[x] -> (mempty, [[lua| %x() |]]))
+    , [luaStmts|
+        local function _Typeable(x)
+          return x()
+        end
+      |] )
+  , ( tcTypeableApp, "_Typeable_app", [], Nothing
+    , [luaStmts|
+        local function _Typeable_app(pair)
+          local ta, tb = pair._1[1], pair._2[1]
+          return { { name = "(" .. ta.name .. ") :$ (" .. tb.name .. ")" } , __tag = "TypeRep" }
+        end
+      |] )
+
+  , ( tcTypeableKnownKnown, "_Typeable_kk", [], Nothing
+    , [luaStmts|
+        local function _Typeable_kk(finger, name)
+          return { { name = name .. "#" .. finger } , __tag = "TypeRep" }
+        end
+      |] )
+
+  , ( tcTYPEREP, "_TypeRep", [], Nothing
+    , [luaStmts|
+        local function _TypeRep(x)
+          return { { name = x.name .. "#" .. x.fingerprint }, __tag = "TypeRep" }
+        end
+      |] )
+  , ( tcUnTypeable, "__type_of", [], Just (1, \[x] -> (mempty, [[lua| function() return %x end |]]))
+    , [luaStmts|
+        local function type_of(x)
+          return function() return x end
+        end
+      |] )
+  , ( tcEqTypeRep, "__eq_type_rep", [], Nothing
+    , [luaStmts|
+        local function __eq_type_rep(tr_a, tr_b, keq, kne)
+          if tr_a[1].name == tr_b[1].name then
+            return keq()() -- n.b.: first argument is ghost of equality proof
+          else
+            return kne()
+          end
+        end
+      |] )
   ]

src/Backend/Lua/Emit.hs

@@ -159,12 +159,24 @@ toGraph = Graph DirectedGraph
         . VarMap.foldrWithKey (\v node xs -> gen v node ++ xs) []
   where
     gen _ EmittedUpvalue{} = []
-    gen var node = Node (defaultInfo { label = Just (display . renderPretty 0.8 100 $ pretty var <> ":=" <> genNode node) }) var
-                   : VarSet.foldr (\var' xs -> Edge defaultInfo var var' : xs) [] (node ^. emitDeps)
-
-    genNode (EmittedExpr expr _ _ _) = vsep . map pretty $ expr
-    genNode (EmittedStmt stmt _ _ _) = vsep . map pretty . toList $ stmt
-    genNode EmittedUpvalue{} = "Upvalue"
+    gen var node
+      = Node (defaultInfo { label = Just (display . renderPretty 0.8 100 $ pretty var <> ":=" <> genNode var node) }) var
+      : ( if var /= main node then [] else
+          VarSet.foldr (\var' xs -> Edge defaultInfo var var' : xs) [] (node ^. emitDeps)
+          ++ VarSet.foldr (\var' xs -> Edge defaultInfo { style = Just Dashed } var' var : xs) [] (VarSet.delete var (node ^. emitBinds)) )
+
+    -- | Try to determine the "primary" node of this term. This is actually
+    -- entirely arbitrary - the only requirement is that it is equal for all
+    -- nodes in this group.
+    main = head . VarSet.toList . (^. emitBinds)
+
+    genNode var node@(EmittedExpr expr _ _ _)
+      | var == main node = vsep . map pretty $ expr
+      | otherwise = "Subsumed with " <+> pretty (main node)
+    genNode var node@(EmittedStmt stmt _ _ _)
+      | var == main node = vsep . map pretty . toList $ stmt
+      | otherwise = "Subsumed with" <+> pretty (main node)
+    genNode _ EmittedUpvalue{} = "Upvalue"
 
 instance IsVar a => Pretty (VarMap.Map (EmittedNode a)) where
   pretty = drawGraph disp . toGraph where
@@ -599,19 +611,19 @@ runNES deps m = do
   pure (deps', binds, a)
 
 withinExpr :: ( Occurs a
-            , MonadReader (EmitScope a) m
-            , MonadState (EmitState a) m )
-         => a -> EmitYield a -> AnnTerm VarSet.Set a
-         -> StateT (NodeEmitState a) m [LuaExpr]
-         -> m ()
+              , MonadReader (EmitScope a) m
+              , MonadState (EmitState a) m )
+           => a -> EmitYield a -> AnnTerm VarSet.Set a
+           -> StateT (NodeEmitState a) m [LuaExpr]
+           -> m ()
 withinExpr var yield term m = withinTerm var term $ flip EmittedExpr yield <$> m
 
 withinTerm :: ( Occurs a
-            , MonadReader (EmitScope a) m
-            , MonadState (EmitState a) m )
-         => a -> AnnTerm VarSet.Set a
-         -> StateT (NodeEmitState a) m (VarSet.Set -> VarSet.Set -> EmittedNode a)
-         -> m ()
+              , MonadReader (EmitScope a) m
+              , MonadState (EmitState a) m )
+           => a -> AnnTerm VarSet.Set a
+           -> StateT (NodeEmitState a) m (VarSet.Set -> VarSet.Set -> EmittedNode a)
+           -> m ()
 withinTerm var term m = do
   ari <- view emitArity
   prev <- use emitPrev
@@ -672,7 +684,8 @@ emitAtom (Ref (toVar -> v) _) = do
           pure expr
     Just (EmittedExpr expr yield binds deps) -> do
       (stmts, vals) <- genYield pushScope' yield expr
-      (nodeState . emitGraph) %= VarMap.insert v (EmittedStmt stmts vals binds deps)
+      let node = EmittedStmt stmts vals binds deps
+      (nodeState . emitGraph) %= \g -> VarSet.foldr (flip VarMap.insert node) g binds
       pure (map unsimple vals)
     where
       -- | Detect if the @emitted@ has a loop
@@ -861,7 +874,7 @@ emitStmt (Foreign n t s:xs) = do
 
           topVars %= VarMap.insert (toVar n)
             ( VarInline (length as) inline
-            , simpleVars [LuaName n'])
+            , simpleVars [LuaName n'] )
           -- This one may never be visited normally, so we'll push the
           -- extra-variable version of it instead.
           topExVars %= VarMap.insert (toVar n) ([], pure $ LuaLocal [LuaName n'] [ex])

src/Control/Monad/Infer.hs

@@ -143,6 +143,9 @@ data TypeError where
   TypeFamInInstHead :: Type Typed -> Type Typed -> TypeError
   InvalidContext :: String -> Span -> Type Desugared -> TypeError
 
+  DIMalformedHead :: SomeReason -> TypeError
+  DICan'tDerive   :: Var Typed -> SomeReason -> TypeError
+
   OrphanInstance :: SomeReason -> Set.Set (Var Typed) -> TypeError
 
   NotAClass :: Var Typed -> TypeError
@@ -485,6 +488,12 @@ instance Pretty TypeError where
   pretty (NotAClass name) =
     vsep [ "Can not make an instance of" <+> pretty name <+> "because it is not a class" ]
 
+  pretty (DIMalformedHead _) =
+    "Malformed head in" <+> keyword "deriving instance" <+> "clause"
+
+  pretty (DICan'tDerive n _) =
+    "Can't derive an instance of class" <+> stypeSkol (pretty n)
+
   pretty (TypeFamInInstHead fun _) =
     vsep [ "Illegal type family application" <+> displayType fun
             <+> "in instance head" ]
@@ -605,6 +614,8 @@ instance Spanned TypeError where
   annotation (UnsatClassCon x _ _) = annotation x
   annotation (TyFamLackingArgs x _ _) = annotation x
   annotation (OrphanInstance x _) = annotation x
+  annotation (DIMalformedHead x) = annotation x
+  annotation (DICan'tDerive _ x) = annotation x
   annotation x = error (show (pretty x))
 
 instance Note TypeError Style where

src/Core/Arity.hs

@@ -129,4 +129,4 @@ mapArity f (Arity a p) = Arity (f a) p
 -- | Various built-in functions with a predetermined arity
 opArity :: VarMap.Map Arity
 opArity = VarMap.fromList . map (flip Arity True <$>) $
-    [ (vLAZY,  2), (vCONS,  2), (vNIL, 1) ]
+  [ (vLAZY,  2), (vCONS,  2), (vNIL, 1), (tcTypeableApp, 4), (tcTypeableKnownKnown, 3) ]

src/Core/Builtin.hs

@@ -28,7 +28,13 @@ vEq, vEQ :: CoVar
 
 tcTypeError, tcErrKind, tcString, tcHCat, tcVCat, tcShowType :: CoVar
 
-[ vBool, vInt, vString, vFloat, vUnit, vLazy, vArrow, vProduct, vList, vRefTy, vKStrTy, vKIntTy, vRowCons, vError, vLAZY, vForce, tyvarA, tyvarB, argvarX, vOpApp, vCONS, vNIL, vAssign, vDeref, vRef, vStrVal, vIntVal, vExtend, vRestrict, vKSTR, vKINT, vROWCONS, tyvarRecord, tyvarNew, tyvarKey, tyvarType, vEq, vEQ, backendRet, backendClone, tcTypeError, tcErrKind, tcString, tcHCat, tcVCat, tcShowType ] = makeBuiltins
+tcTypeable, tcTypeRep, tcUnTypeable, tcTYPEABLE, tcTYPEREP, tcEqTypeRep :: CoVar
+tyvarKind :: CoVar
+tyvarProxy :: CoVar
+
+tcTypeableApp, tcTypeableKnownKnown :: CoVar
+
+[ vBool, vInt, vString, vFloat, vUnit, vLazy, vArrow, vProduct, vList, vRefTy, vKStrTy, vKIntTy, vRowCons, vError, vLAZY, vForce, tyvarA, tyvarB, argvarX, vOpApp, vCONS, vNIL, vAssign, vDeref, vRef, vStrVal, vIntVal, vExtend, vRestrict, vKSTR, vKINT, vROWCONS, tyvarRecord, tyvarNew, tyvarKey, tyvarType, vEq, vEQ, backendRet, backendClone, tcTypeError, tcErrKind, tcString, tcHCat, tcVCat, tcShowType, tcTypeable, tcUnTypeable, tcTypeRep, tcTYPEABLE, tcTYPEREP, tcEqTypeRep, tcTypeableApp, tcTypeableKnownKnown, tyvarKind, tyvarProxy ] = makeBuiltins
   [ ("bool", TypeConVar)
   , ("int", TypeConVar)
   , ("string", TypeConVar)
@@ -89,6 +95,17 @@ tcTypeError, tcErrKind, tcString, tcHCat, tcVCat, tcShowType :: CoVar
   , (":<>:", DataConVar)
   , (":<#>:", DataConVar)
   , ("ShowType", DataConVar)
+
+  , ("typeable", TypeConVar)
+  , ("type_of", ValueVar)
+  , ("type_rep", TypeConVar)
+  , ("$Typeable", ValueVar)
+  , ("$TypeRep", ValueVar)
+  , ("eq_type_rep", ValueVar)
+  , ("$TypeableApp", ValueVar)
+  , ("$TypeableKK", ValueVar)
+  , ("kind", TypeVar)
+  , ("proxy", TypeVar)
   ]
 
 tyBool, tyInt, tyString, tyFloat, tyUnit, tyLazy, tyList, tyRef, tyKStr, tyKInt, tyRowCons, tyEq :: IsVar a => Type a
@@ -127,6 +144,8 @@ builtinTyList = [ fromVar vBool
                 , fromVar tcVCat
                 , fromVar tcString
                 , fromVar tcTypeError
+                , fromVar tcTypeable
+                , fromVar tcTypeRep
                 ]
 
 builtinVarList :: forall a b. (IsVar a, IsVar b) => [(a, Type b)]
@@ -137,13 +156,14 @@ builtinVarList = vars where
   arrTy = ForallTy Irrelevant
   prodTy a b = RowsTy NilTy [("_1", a), ("_2", b)]
 
-  name, name', record, ttype, key, new :: b
+  name, name', record, ttype, key, new, proxy :: b
   name = fromVar tyvarA
   name' = fromVar tyvarB
   record = fromVar tyvarRecord
   ttype = fromVar tyvarType
   key = fromVar tyvarKey
   new = fromVar tyvarNew
+  proxy = fromVar tyvarProxy
 
   appsTy :: [Type b] -> Type b
   appsTy = foldl1 AppTy
@@ -171,6 +191,46 @@ builtinVarList = vars where
          , op vIntVal (ForallTy (Relevant name) tyInt $ AppTy tyKInt (VarTy name) `arrTy` tyInt)
          , op vKINT (ForallTy (Relevant name) tyInt $ tyInt `arrTy` AppTy tyKInt (VarTy name))
 
+         , op tcTYPEABLE
+             ( ForallTy (Relevant name) StarTy
+             $ ForallTy (Relevant proxy) StarTy (AppTy (VarTy proxy) (VarTy name) `arrTy` AppTy (ConTy (fromVar tcTypeRep)) (VarTy name))
+                 `arrTy` AppTy (ConTy (fromVar tcTypeable)) (VarTy name))
+
+         , op tcTYPEREP (ForallTy (Relevant name) StarTy
+                          $ ExactRowsTy [ ("fingerprint", tyInt)
+                                        , ("name", tyString) ]
+                    `arrTy` AppTy (ConTy (fromVar tcTypeRep)) (VarTy name))
+
+         , op tcEqTypeRep ( ForallTy (Relevant name) StarTy
+                          $ ForallTy (Relevant name') StarTy
+                          $ ForallTy (Relevant new) StarTy
+                          $ tupTy [ AppTy (ConTy (fromVar tcTypeRep)) (VarTy name)
+                                  , AppTy (ConTy (fromVar tcTypeRep)) (VarTy name')
+                                  , appsTy [ tyEq, VarTy name, VarTy name' ]
+                                      `arrTy` (tyUnit `arrTy` VarTy new)
+                                  , tyUnit `arrTy` VarTy new ]
+                              `arrTy` VarTy new)
+
+         , op tcUnTypeable ( ForallTy (Relevant name) StarTy
+                           $ ForallTy (Relevant proxy) StarTy
+                           $ AppTy (ConTy (fromVar tcTypeable)) (VarTy name)
+                     `arrTy` (AppTy (VarTy proxy) (VarTy name)
+                     `arrTy` AppTy (ConTy (fromVar tcTypeRep)) (VarTy name)))
+
+         , op tcTypeableApp ( ForallTy (Relevant name) StarTy
+                            $ ForallTy (Relevant name') StarTy
+                            $ (AppTy (ConTy (fromVar tcTypeable)) (VarTy name)
+                                `prodTy` AppTy (ConTy (fromVar tcTypeable)) (VarTy name'))
+                               `arrTy` AppTy (ConTy (fromVar tcTypeable)) (AppTy (VarTy name) (VarTy name'))
+                            )
+
+         , op tcTypeableKnownKnown
+              ( ForallTy (Relevant name) StarTy
+              $ tupTy [ AppTy tyKInt StarTy
+                      , AppTy tyKStr StarTy
+                      ]
+                 `arrTy` AppTy (ConTy (fromVar tcTypeable)) (VarTy name))
+
          , op vExtend $
              ForallTy (Relevant key) tyString $
                ForallTy (Relevant record) StarTy $

src/Core/Lower.hs

@@ -329,6 +329,7 @@ lowerProg' (Class{}:prg) = lowerProg' prg
 lowerProg' (Instance{}:prg) = lowerProg' prg
 lowerProg' (TySymDecl{}:prg) = lowerProg' prg
 lowerProg' (TypeFunDecl{}:prg) = lowerProg' prg
+lowerProg' (DeriveInstance{}:prg) = lowerProg' prg
 
 lowerProg' (ForeignVal _ v ex tp _:prg) =
   let tyB = lowerType tp
@@ -561,4 +562,6 @@ boxedTys = VarMap.fromList
            $ C.builtinVarList where
   boxed = VarSet.fromList
     [ C.vOpApp, C.vAssign, C.vExtend, C.vRestrict
+    , C.tcEqTypeRep
+    , C.tcTypeableApp, C.tcTypeableKnownKnown
     ]

src/Parser.y

@@ -115,6 +115,7 @@ import Syntax
   when     { Token TcWhen _ _ }
   private  { Token TcPrivate _ _ }
   include  { Token TcInclude _ _ }
+  deriving { Token TcDeriving _ _ }
 
   ','      { Token TcComma _ _ }
   '.'      { Token TcDot _ _ }
@@ -207,6 +208,7 @@ Top :: { Toplevel Parsed }
         {% fmap (withPos2 $1 $5) $ buildClass Private $3 $4 (getL $5) }
 
     | instance Type Begin(Methods)             {% fmap (withPos2 $1 $3) $ buildInstance $2 (getL $3) }
+    | deriving Type                            { withPos2 $1 $2 $ DeriveInstance (getL $2) }
 
 TyFunBody :: { [TyFunClause Parsed] }
   : List(TyFunEq, TopSep) { $1 }
@@ -734,10 +736,10 @@ buildInstance (L ty typ) ms =
   case ty of
     (TyPi (Implicit ctx) ty) -> do
       name <- go ty
-      pure (Instance name (Just ctx) ty ms)
+      pure (Instance name (Just ctx) ty ms False)
     ty -> do
       name <- go ty
-      pure (Instance name Nothing ty ms)
+      pure (Instance name Nothing ty ms False)
   where
     go :: Type Parsed -> Parser (Var Parsed)
     go (TyCon v) = pure v

src/Parser/Context.hs

@@ -593,6 +593,7 @@ isTopTok TcType = True
 isTopTok TcVal = True
 isTopTok TcPrivate = True
 isTopTok TcOpen = True
+isTopTok TcDeriving = True
 isTopTok _ = False
 
 -- | Get the left most margin of the current context

src/Parser/Lexer.x

@@ -102,6 +102,7 @@ tokens :-
   <0> "when"     { constTok TcWhen }
   <0> "private"  { constTok TcPrivate }
   <0> "include"  { constTok TcInclude }
+  <0> "deriving" { constTok TcDeriving }
 
   <0> ","      { constTok TcComma }
   <0> "."      { constTok TcDot }