12
$\begingroup$

How does it compare to dependent records in Agda/Lean/etc.?

I heard that locales in Isabelle are used to model algebraic structures in a talk, bu. Isn't this a kind of dependent type in some sense? Is Isabelle really simply typed?

$\endgroup$
1
  • 4
    $\begingroup$ AFAIR the main limitation is that they are not first-class. They are not too different from a module system; $\endgroup$ Feb 8, 2022 at 18:37

1 Answer 1

12
$\begingroup$

Basically, a locale is a name for a set of fixed parameters, that come with assumptions. Inside the locale, these assumptions are added implicitly to everything you define/prove. When you have concrete parameters that satisfy the assumptions, you can interpret the locale, exposing the stuff inside (instantiated for your concrete parameters).

In Isabelle, locales are quite powerful. You can base your locales on other locales, partially instantiate them, rewrite stuff, etc. (for details https://isabelle.in.tum.de/dist/Isabelle2021-1/doc/locales.pdf)

$\endgroup$
5
  • $\begingroup$ Without reading the link, isn't that a dependent type? $\endgroup$
    – ice1000
    Feb 8, 2022 at 21:53
  • $\begingroup$ @ice1000 it is merely a way of organizing contexts (parameters and assumptions) and quite limited compared to usual module systems (eg. you can not define new types). I am not sure I understand, what makes you think that they are dependent types? $\endgroup$
    – Wno-all
    Feb 9, 2022 at 22:02
  • $\begingroup$ You can define functions inside a locale, but no types (functions and types are separate concepts in hol). So no type depending on locale assumptions possible. $\endgroup$ Feb 9, 2022 at 22:48
  • 1
    $\begingroup$ Besides implicit assumptions one thing that locales are useful for is limiting the scope of notation. It happens quite often in standard mathematics that the meaning of notation depends on the context. A symbol can mean different things in different contexts and different symbols can have essentially the same meaning in different contexts (e.g. in group theory one can use additive or multiplicative notation). With locales one can set up context-dependent notation in Isar and then use the sublocale keyword to specify how this notation maps to the notation in a different context (locale). $\endgroup$ Feb 10, 2022 at 19:28
  • $\begingroup$ @ice1000 IIUC, to pass a monoid via locales, Isabelle you pass the pieces separately: then you only need usual HOL + simple types. $\endgroup$ Feb 20, 2022 at 13:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.