search

UCSD-PL / refscript

Refinement Types for Scripting Languages
BSD 3-Clause "New" or "Revised" License
65 stars 3 forks source link

Conditional Expressions #41

Closed panagosg7 closed 10 years ago

panagosg7 commented 10 years ago 
e ? e1 : e2

Issue #38 is addressed by means of contextual typing.

If a contextual type is present it is used to cast e1 and e2. The casting happens only in the raw level.

So the original becomes:

e ? <T> e1 : <T> e2

In Liquid it is assumed that the base types for e1 and e2 are the same and so we can use a "modified" version of function call to a function with signature:

condExpr :: forall C A . (c: C, x: A, y: A) => { v: A | if Prop(c) then v ~~ x else x ~~ y }

The modified version makes sure that the arguments e1 and e2 are compiled under the guards: True(c) and False(c) respectively.

ranjitjhala commented 10 years ago

This is a nice solution -- I thought this would be a lot harder :)