5 ms·

I was also surprised. The syntax they use is basically Standard ML. Also I'd really like to see a paper on their static type checking, because they mix objects

I was also surprised. The syntax they use is basically Standard ML. Also I'd really like to see a paper on their static type checking, because they mix objects and algebraic data types, which is not trivial at all.

mkolosick 10y 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!
- throw_again99 10y ago
  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/bed2822602ed37484c166cef1d57f7be.en.html 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
  - mkolosick 10y 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`.
    - throw_again99 10y ago
      This is rather nice. You get a lot of convenience for that one type annotation!
  - skrishnamurthi 10y ago
    To add to @mkolosick's reply: Pyret doesn't have classes and hence class "hierarchies".

mkolosick 10y 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!

throw_again99 10y ago
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/bed2822602ed37484c166cef1d57f7be.en.html 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
- mkolosick 10y 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`.
  - throw_again99 10y ago
    This is rather nice. You get a lot of convenience for that one type annotation!
- skrishnamurthi 10y ago
  To add to @mkolosick's reply: Pyret doesn't have classes and hence class "hierarchies".