While naming the different derivation rules can be useful for guiding readers the names are not formally necessary.

The rules

  A   B
  -----
    C

and

  A   B
  ----- (→c)
    C

are logically equivalent, the latter just gives you a name to refer to the rule by.

Additionally, I would be careful about correcting others that something is "technically" called something else as programming language researchers often use many names for the same concept.

> Additionally, I would be careful about correcting others that something is "technically" called something else as programming language researchers often use many names for the same concept.

My point had nothing to do with programming language research (in fact, my academic background is logic/metalogic). And by the way, this is not a rule:

    A   B
    ----- (→c)
      C

It's a derivation (also known as a proof) -- technical terms are important when doing logic. The rule is →c -- so I know what you're doing by including the →c there. Why the →c is necessary (and, again, I've seen it in every lambda calculus/type theory book I've taken a gander at) is because there are many rules[1] (including several kinds of elimination, so things can get complicated and it's important to keep our ducks in a row).

[1] https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/Selinger-L...

Perhaps using abstract names A, B, and C was unclear. The following is the rule that is commonly referred to as modus ponens:

  A → B    A
  -----------
       B 

However, modus ponens is just one of the names for this. I could also call it function elimination. I could call it →e. Or I could not bother giving it a name and just say that this is a rule in my logic call it whatever you want in your head if you so desire.

Things can get complicated, but they aren't always complicated so naming rules isn't strictly necessary.

Hi, I'm actually the person who wrote the static type checker. Essentially we get around the difficulties of mixing objects and ADTs by having very limited support for subtyping. This way we can still carry out unification-based inference. The subtyping bounds are not propagated during unification so we don't need to worry about calculating closures. This does mean that type inference is incomplete with respect to subtyping, but I haven't found a satisfactory system that would let us do otherwise.

I would also like to note that we do also have a new feature where types can be inferred if you provide tests in a "where:" block attached to a function. This infers a function's type solely from the examples of usage provided.

If you have any other questions feel free to ask!

Hi, thanks. Primarily I wondered about actual mixing of ADTs and objects, which is limited even in OCaml, see e.g.:

http://caml.inria.fr/pub/ml-archives/caml-list/2003/06/bed28...

But does Pyret always translate an ADT to a class hierarchy behind the scenes? This example sure looks like it does:

  data Animal:
    | elephant(name, weight)
    | tiger(name, stripes)
    | horse(name, races-won)
    ...
  end

  fun animal-name(a :: Animal):
    a.name
  end

Good question! Pyret does not translate to a class hierarchy. Pyret dynamically allows dot lookups on both objects and ADTs. In the type checker this means that an ADT permits dot lookup on any field that all variants have (in this case, `name`), as this will always be safe.

Additionally, Pyret's type system internally tracks each of the different constructors as a refinement on the type. With the animal example this would be represented internally as something like

  Animal%(is-elephant)

if the type is known to only be an elephant. Though this is not used everywhere it could be right now it is part of the system. This means we have room to do things like if-splitting e.g.

  if is-elephant(x): ...

would be able to treat x as an

  Animal%(is-elephant)

in the body rather than just an `Animal`.

This is rather nice. You get a lot of convenience for that one type annotation!

To add to @mkolosick's reply: Pyret doesn't have classes and hence class "hierarchies".

You can use "!hn duckduckgo" that usually works better.

I doubt that works "better" and certainly there is no bang for every site.

As the sibling comment mentions, Pyret was originally written in Racket. It's now self-hosted, and I'm working on rewriting the typechecker so if you want I can answer questions about that. The current development is all done on https://github.com/brownplt/pyret-lang

How do you determine semantically equivalent code fragments? Is it a dynamic solution or a static solution?

Not quite though. I had a bug with Javascript where I was reading in a number and forgot to parse it to a float. I ended up doing an addition with that value, which later got used as a float again. So I had 1 + "10" turn to 110 when I tried to use it. No == or === anywhere.

I was only really referring to automatic type conversion for comparisons. That said, the example you gave sounds like the opposite, where you wanted it to do some auto-conversion and you're disappointed that it didn't? If I did 1 + "10" I don't think I'd want it to return 11!

I'd want it to throw some kind of cast exception, personally, not try and do what it thinks I want. (I'm not the GP)

It did convert the value. It converted the 1 to a string and added "10" to the end of it, resulting in "110" which then was converted to a float and used.

The error in this case would be forgetting Javascript's rules of implicit conversion.

Adding a float to a string results in a string.

It's more a one-way dataflow language.