search

anoma / juvix

A language for intent-centric and declarative decentralised applications
https://docs.juvix.org
GNU General Public License v3.0
457 stars 53 forks source link

Isabelle/HOL: translate traits to type classes or locales #2893

Open lukaszcz opened 4 months ago

lukaszcz commented 4 months ago
lukaszcz commented 2 weeks ago

Comment by @AHartNtkn (for future reference):

I would put the definitions within a dummy context and instantiate them when instances are made. For example, 

locale option
interpretation option .

context option (* Maybe Functor *) begin

definition map :: "('a ⇒ 'b) ⇒ 'a option ⇒ 'b option" where
  "map f m = (
   case m of
    (Some x) ⇒ Some (f x) |
    None ⇒ None
)"

end

value "option.map (λx. x+1) (Some (2::nat))"

context option (* Maybe Applicative *) begin

definition pure :: "'a ⇒ 'a option" where
  "pure x = Some x"

end

context option (* Maybe Monad *) begin

definition bind :: "'a option ⇒ ('a ⇒ 'b option) ⇒ 'b option" where
  "bind m f = (
    case m of
      (Some x) ⇒ (f x) |
      None ⇒ None
  )"

end

and when new functions for the specific instances are declared, the context can be reused. When instances are used, they have to be qualified by the context name, so option.bind, etc. I don't believe there's a better solution.