HN user

mkolosick

14 karma
Posts0
Comments9
View on HN
No posts found.
Higher-order logic and equality; multiple ways to use lambda calculus for logic 6 years ago

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.

0ThreadHN
Higher-order logic and equality; multiple ways to use lambda calculus for logic 6 years ago

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.

0ThreadHN
Pyret – A language exploring scripting and functional programming 10 years ago

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`.
0ThreadHN
Pyret – A language exploring scripting and functional programming 10 years ago

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!

0ThreadHN
ES6 in Depth – Symbols 11 years ago

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.

0ThreadHN