A Hugo incarnation of the blog.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

TypesafeIntrV2.idr 3.2KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899
  1. data ExprType
  2. = IntType
  3. | BoolType
  4. | StringType
  5. repr : ExprType -> Type
  6. repr IntType = Int
  7. repr BoolType = Bool
  8. repr StringType = String
  9. intBoolImpossible : IntType = BoolType -> Void
  10. intBoolImpossible Refl impossible
  11. intStringImpossible : IntType = StringType -> Void
  12. intStringImpossible Refl impossible
  13. boolStringImpossible : BoolType = StringType -> Void
  14. boolStringImpossible Refl impossible
  15. decEq : (a : ExprType) -> (b : ExprType) -> Dec (a = b)
  16. decEq IntType IntType = Yes Refl
  17. decEq BoolType BoolType = Yes Refl
  18. decEq StringType StringType = Yes Refl
  19. decEq IntType BoolType = No intBoolImpossible
  20. decEq BoolType IntType = No $ intBoolImpossible . sym
  21. decEq IntType StringType = No intStringImpossible
  22. decEq StringType IntType = No $ intStringImpossible . sym
  23. decEq BoolType StringType = No boolStringImpossible
  24. decEq StringType BoolType = No $ boolStringImpossible . sym
  25. data Op
  26. = Add
  27. | Subtract
  28. | Multiply
  29. | Divide
  30. data Expr
  31. = IntLit Int
  32. | BoolLit Bool
  33. | StringLit String
  34. | BinOp Op Expr Expr
  35. | IfElse Expr Expr Expr
  36. data SafeExpr : ExprType -> Type where
  37. IntLiteral : Int -> SafeExpr IntType
  38. BoolLiteral : Bool -> SafeExpr BoolType
  39. StringLiteral : String -> SafeExpr StringType
  40. BinOperation : (repr a -> repr b -> repr c) -> SafeExpr a -> SafeExpr b -> SafeExpr c
  41. IfThenElse : SafeExpr BoolType -> SafeExpr t -> SafeExpr t -> SafeExpr t
  42. typecheckOp : Op -> (a : ExprType) -> (b : ExprType) -> Either String (c : ExprType ** repr a -> repr b -> repr c)
  43. typecheckOp Add IntType IntType = Right (IntType ** (+))
  44. typecheckOp Subtract IntType IntType = Right (IntType ** (-))
  45. typecheckOp Multiply IntType IntType = Right (IntType ** (*))
  46. typecheckOp Divide IntType IntType = Right (IntType ** div)
  47. typecheckOp _ _ _ = Left "Invalid binary operator application"
  48. requireBool : (n : ExprType ** SafeExpr n) -> Either String (SafeExpr BoolType)
  49. requireBool (BoolType ** e) = Right e
  50. requireBool _ = Left "Not a boolean."
  51. typecheck : Expr -> Either String (n : ExprType ** SafeExpr n)
  52. typecheck (IntLit i) = Right (_ ** IntLiteral i)
  53. typecheck (BoolLit b) = Right (_ ** BoolLiteral b)
  54. typecheck (StringLit s) = Right (_ ** StringLiteral s)
  55. typecheck (BinOp o l r) = do
  56. (lt ** le) <- typecheck l
  57. (rt ** re) <- typecheck r
  58. (ot ** f) <- typecheckOp o lt rt
  59. pure (_ ** BinOperation f le re)
  60. typecheck (IfElse c t e) =
  61. do
  62. ce <- typecheck c >>= requireBool
  63. (tt ** te) <- typecheck t
  64. (et ** ee) <- typecheck e
  65. case decEq tt et of
  66. Yes p => pure (_ ** IfThenElse ce (replace p te) ee)
  67. No _ => Left "Incompatible branch types."
  68. eval : SafeExpr t -> repr t
  69. eval (IntLiteral i) = i
  70. eval (BoolLiteral b) = b
  71. eval (StringLiteral s) = s
  72. eval (BinOperation f l r) = f (eval l) (eval r)
  73. eval (IfThenElse c t e) = if (eval c) then (eval t) else (eval e)
  74. resultStr : {t : ExprType} -> repr t -> String
  75. resultStr {t=IntType} i = show i
  76. resultStr {t=BoolType} b = show b
  77. resultStr {t=StringType} s = show s
  78. tryEval : Expr -> String
  79. tryEval ex =
  80. case typecheck ex of
  81. Left err => "Type error: " ++ err
  82. Right (t ** e) => resultStr $ eval {t} e
  83. main : IO ()
  84. main = putStrLn $ tryEval $ BinOp Add (IfElse (BoolLit True) (IntLit 6) (IntLit 7)) (BinOp Multiply (IntLit 160) (IntLit 2))