[isabelle-dev] Sort constraints [was: Tweak Haskell output for future Haskell compatibility.]

[Florian Haftmann]

Hi all,

just a synopsis of the whole matter of sort constraints for constants.

a) Sort constraints for code generation.  Concerning sort constraints
and datatype constructors, everything has been said already in this
thread.  Generally, for code generation sort constraints *have*
operational relevance.  This is a fundamental difference to the logic
itself where there is no notion of execution.

b) Sort constraints have *no* logical relevance.  Indeed, given a

definition foo :: "'a::s" where
  "foo ['a::s] = rhs"

is internally stored as
  "foo [?'a::{}] == rhs"

which is the »most correct« form of a definition because only then it is
definitional: foo [?'a::{}] can be unfolded for arbitrary instances of
?'a . Note that foo_def carries a sort constraint for 'a; this is an
example how a specification by definition may be more special than the
underlying primitive definition, and is not restricted to sort
constraints, e.g. as in:

definition foo :: "'a::s" where
  "P ==> foo ['a::s] = rhs"

c) Sort constraints as syntactic device.  Here the parser is instructed
to enfore sort constraints on constants.

Hope this helps,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120513/0465fe3f/attachment.sig>