search

diprism / perpl

The PERPL Compiler
MIT License
10 stars 5 forks source link

Syntax for `sample` #39

Closed colin-mcd closed 2 years ago

colin-mcd commented 2 years ago

We currently allow both amb a b ... z (where a, b, ..., z all have the same type, and each get weight 1) and sample amb : TYPE (which assigns weight 1 to all inhabitants of TYPE). But we it would be nice to pick one form of the syntax.

Some options/ideas:

  1. amb a b ... z, uniform a b ... z, fail : TYPE
  2. sample amb : TYPE, sample uniform : TYPE, sample fail : TYPE
  3. amb a b ... z, factor FLOAT, fail (where factor multiplies branch weight by a float, and fail has type Unit)

In practice, option (1) has felt nicer to write code with because of how annoying it is if you want to amb 3 terms: amb a b c vs if (sample amb : Bool) then a else if (sample amb : Bool) then b else c. But because we synthesize types, (1) needs fail to have : TYPE after it in contrast to amb and uniform. @davidweichiang suggested option (3), which seems pretty nice.

davidweichiang commented 2 years ago

In (3), factor FLOAT either needs to return unit or have a type, right? Although fail can have type Unit, I imagine there are lots of situations where that's not convenient, so it's probably best for it to have a type.

ccshan commented 2 years ago

I don't remember the concrete experience to justify it anymore, but I agree that fail at arbitrary (hence specified) type is good to have. In Hakaru (cue harp music) we indeed had fail require explicit : TYPE, and prohibited nullary amb.

The only reason I see for the extra sample is that some languages have weak transforms that cannot deal with distributions built with "bind", and sample distinguishes those distributions that are not built with "bind".

factor FLOAT (implicitly of type unit) is nice to have. I am neutral about whether to provide uniform.

ccshan commented 2 years ago

Unlike (1) and (3), only sample amb : TYPE (which I would just write as amb : TYPE) allows someone to express the "flat" "distribution" without caring what TYPE is. For all they know, TYPE is a function type, and our nonstandard interpretation of functions kicks in. I don't know that we need to allow this in the implementation.

davidweichiang commented 2 years ago

Maybe it's not great that amb (as opposed to sample amb) is equivalent to fail.