1. 9

  2. 2

    Very interesting to see the parallels between MacroML and Shen lisp Both support type-safe macros, both work in stages, and both have a small core language which the other stages are built on top of. The primary difference is that MacroML is based on CoreML, whereas Shen is based on klambda.

    1. 2

      Does Shen have an equivalent to the formal semantics described in there that guarantee the properties they want? Or does it use its Sequent Calculus component for everything?

      1. 2

        Is sequent calculus not formal enough? (Honest question, I don’t have much training in the way of formal methods.)

        Poking around one of Mark Tarver’s more recent papers:

        In Shen, types are defined in the notation of a single-conclusion sequent calculus. Sequent calculus has a long tradition in logic stemming from Gentzen’s foundational work in the area. It was taken up by many authors (e.g [6], [21]) to specify formal systems including type theories.

        1. Cardelli L. Basic Polymorphic Type Checking, Science of Computer Programming, 1987.

        2. Thompson S. Type Theory and Functional Programming, Addison-Wesley, 1991.

        As I understand things, formal deduction is usually done in “Hilbert-style”, in which each additional assertion is an unconditional tautology. This is in contrast with “Gentzen-style”, in which each additional assertion is a conditional tautology. Sequent calculus is a Gentzen-style form, where each statement may have zero or more conditions. Everything I’m reading about it says sequent calculus is a “sound and complete” system of proof-making.

        1. 1

          Im with you in not being formal enough to know. What Im trying to assess most is whether Shen’s is lower level and decidable like FOL or higher-level with more manual work like HOL. My initial guess was it’s more like the former given nature of how it’s used.