icicle-lang / icicle-ambiata

A streaming query language.
BSD 3-Clause "New" or "Revised" License
57 stars 11 forks source link

Discharge join constraints in the function typechecker #668

Closed HuwCampbell closed 5 years ago

HuwCampbell commented 6 years ago

We should be able to run these discharges in the function definitions, as they are self contained.

With this change, the type of any becomes

any : Element Bool -> Aggregate Bool

instead of

any :
     d =: PossibilityJoin c d
  => c =: PossibilityJoin a d
  => Element =: TemporalityJoin b Element
  => b (a Bool)
  -> Aggregate (c Bool)