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?
$\begingroup$
$\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$– Sebastian UllrichCommented Feb 8, 2022 at 18:37
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
5
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)
-
$\begingroup$ Without reading the link, isn't that a dependent type? $\endgroup$– ice1000 ♦Commented 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-allCommented 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$ Commented 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
sublocalekeyword to specify how this notation maps to the notation in a different context (locale). $\endgroup$ Commented 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$ Commented Feb 20, 2022 at 13:43