<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">Hi Erick,<div><br class="webkit-block-placeholder"></div><div>On 2008-03-15, at 04:03, Erick Tryzelaar wrote:</div><div><br class="webkit-block-placeholder"></div><div><div><div><div><div><div><div><div><div></div></div></div></div></div></div></div></div></div><div><div><span class="Apple-style-span" style="-webkit-text-stroke-width: -1; "><div><blockquote type="cite">I was talking to Gordon on #llvm earlier, and he challenged me with coming up with a way to improve the ocaml binding's type safety. I think I got an easy solution with phantom types.</blockquote><div><br class="webkit-block-placeholder"></div><span class="Apple-style-span" style="-webkit-text-stroke-width: 0; ">This could be a good step. I'm not sure I can predict all of the implications; I'd suggest you work up a proof of concept.<div><div><div><br class="webkit-block-placeholder"></div><div>The <font class="Apple-style-span" face="Courier">Value</font> hierarchy is very complicated; it will take much work to apply this technique there, so I would suggest that be a second step. A similar but smaller problem presents itself in the <font class="Apple-style-span" face="Courier">Type</font> hierarchy, which is (relatively speaking) simple. You may be able to implement type safety for <font class="Apple-style-span" face="Courier">Type</font> as a layer on top of the existing bindings, or at least on top of the existing glue; you should have sufficient flexibility to do so because we do expose the <font class="Apple-style-span" face="Courier">TypeID</font> enum via <font class="Apple-style-span" face="Courier">classify_type</font>.</div><div><div><br class="webkit-block-placeholder"></div><div><div><div><div>In order to be useful, I think it will also be necessary to provide a new class of functions, a set of type checking helpers which play the same role as <font class="Apple-style-span" face="Courier">bool T::isa<U>(T*)</font>, <font class="Apple-style-span" face="Courier">U* T::cast<U>(T*)</font>, and <font class="Apple-style-span" face="Courier">U* T::dyn_cast<U>(T*)</font>:</div><div><br class="webkit-block-placeholder"></div></div></div></div></div></div><blockquote class="webkit-indent-blockquote" style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 40px; border-top-style: none; border-right-style: none; border-bottom-style: none; border-left-style: none; border-width: initial; border-color: initial; padding-top: 0px; padding-right: 0px; padding-bottom: 0px; padding-left: 0px; "><span class="Apple-style-span" style="font-family: Courier; "><font class="Apple-style-span" color="#FF0000">(** @see [bool Type::isa<FunctionType>(Type*)] *)</font></span><font class="Apple-style-span" color="#FF0000"><br></font><span class="Apple-style-span" style="font-family: Courier; "><font class="Apple-style-span" color="#0000FF">val</font> is_function_type : lltype t -> bool</span><br><br><span class="Apple-style-span" style="font-family: Courier; "><font class="Apple-style-span" color="#FF0000">(** @see [FunctionType *Type::dyn_cast<FunctionType>(Type*)]</font></span><font class="Apple-style-span" color="#FF0000"><br></font><span class="Apple-style-span" style="font-family: Courier; "><font class="Apple-style-span" color="#FF0000"> @raise Invalid_cast if the conversion is impossible. *)</font></span><font class="Apple-style-span" color="#FF0000"><br></font><span class="Apple-style-span" style="font-family: Courier; "><font class="Apple-style-span" color="#0000FF">val</font> as_function_type : lltype t -> `FunctionTy t</span></blockquote><div><div><div><div><div><div><br></div><div>For <font class="Apple-style-span" face="Courier">Value</font>, it will be important to push the ISA routines through all of the layers (esp. for <font class="Apple-style-span" face="Courier">Value</font>), but I think you can implement ISA routines in Ocaml relatively painlessly for <font class="Apple-style-span" face="Courier">Type</font>.</div></div></div></div></div></div></div></span></div></span></div></div><div><div><span class="Apple-style-span" style="-webkit-text-stroke-width: -1; "><div><span class="Apple-style-span" style="-webkit-text-stroke-width: 0; "><div><div><div><div><div><div><div><br class="webkit-block-placeholder"></div></div></div></div></div></div></div><div><span class="Apple-style-span" style="-webkit-text-stroke-width: -1; "><div></div></span></div></span><blockquote type="cite">Here's the full example:<br><br>foo.mli:<br>type 'a t<br>type llvalue = [ `Value ]<br>type llfunction = [ llvalue | `Function ]<br><br>val use_value : [> `Value] t -> unit<br>val use_function : [> `Function] t -> unit<br><br>val make_value : unit -> llvalue t<br>val make_function : unit -> llfunction t<br><br>Does this sound like it could work, or am I missing something?<br></blockquote></div></span></div><div><br class="webkit-block-placeholder"></div><div>I think your sum types are incorrect here. <font class="Apple-style-span" face="Courier">Value</font> is abstract; I think you want to say something like:</div><div><br class="webkit-block-placeholder"></div><blockquote class="webkit-indent-blockquote" style="margin: 0 0 0 40px; border: none; padding: 0px;"><font class="Apple-style-span" face="Courier">type llglobal = [ `GlobalVariable | `Function | ... ]</font></blockquote><blockquote class="webkit-indent-blockquote" style="margin: 0 0 0 40px; border: none; padding: 0px;"><font class="Apple-style-span" face="Courier">type llconst = [ llglobal | `ConstantInt | ... ]<br>type llany = [ llconst | ... ]</font></blockquote><div><br class="webkit-block-placeholder"></div><div>With only the concrete classes given tags. (doxygen is your friend here.) Try mocking up the type system for the concrete types <font class="Apple-style-span" face="Courier">GlobalVariable</font>, <font class="Apple-style-span" face="Courier">Function<span class="Apple-style-span" style="font-family: 'Trebuchet MS'; ">, <font class="Apple-style-span" face="Courier">ConstantFP<span class="Apple-style-span" style="font-family: 'Trebuchet MS'; "> and <font class="Apple-style-span" face="Courier">ConstantInt</font>; the abstract types <font class="Apple-style-span" face="Courier">GlobalValue</font>, <font class="Apple-style-span" face="Courier">Value<span class="Apple-style-span" style="font-family: 'Trebuchet MS'; "> and </span>Constant<span class="Apple-style-span" style="font-family: 'Trebuchet MS'; ">; and the functions <span class="Apple-style-span" style="font-family: Courier; ">set_value_name<span class="Apple-style-span" style="font-family: 'Trebuchet MS'; ">, <span class="Apple-style-span" style="font-family: Courier; ">linkage<span class="Apple-style-span" style="font-family: 'Trebuchet MS'; ">, </span>declare_global<span class="Apple-style-span" style="font-family: 'Trebuchet MS'; ">, </span>set_initializer<span class="Apple-style-span" style="font-family: 'Trebuchet MS'; ">, <span class="Apple-style-span" style="font-family: Courier; ">declare_function<span class="Apple-style-span" style="font-family: 'Trebuchet MS'; ">, <span class="Apple-style-span" style="font-family: Courier; "><span class="Apple-style-span" style="font-family: 'Trebuchet MS'; "><span class="Apple-style-span" style="font-family: Courier; ">entry_block<span class="Apple-style-span" style="font-family: 'Trebuchet MS'; ">, <span class="Apple-style-span" style="font-family: Courier; ">param<span class="Apple-style-span" style="font-family: 'Trebuchet MS'; "><span class="Apple-style-span" style="font-family: Courier; "><span class="Apple-style-span" style="font-family: 'Trebuchet MS'; ">, </span>const_float<span class="Apple-style-span" style="font-family: 'Trebuchet MS'; ">, </span>const_int<span class="Apple-style-span" style="font-family: 'Trebuchet MS'; ">, and </span>const_array<span class="Apple-style-span" style="font-family: 'Trebuchet MS'; ">. That should be a reasonable survey.</span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></font></span></font></span></font></div><div><br class="webkit-block-placeholder"></div><div><div><div><div><div><div><div><div><blockquote type="cite">We can't go letting haskell beat us now, can we?<br></blockquote><div><br class="webkit-block-placeholder"></div>To truly compete with Bryan's Haskell bindings in terms of type safety, you'll need to go beyond preventing the cast macros in the C bindings from asserting and actually take over some of the work performed by the verifier. This is very difficult to do correctly outside of toy programs. For instance, given <font class="Apple-style-span" face="Courier">const_add x y</font>, there are several conditions that would be interesting for the type checker to verify:</div><div><br class="webkit-block-placeholder"></div></div></div></div></div></div></div></div><blockquote class="webkit-indent-blockquote" style="margin: 0 0 0 40px; border: none; padding: 0px;"><font class="Apple-style-span" face="Courier"><font class="Apple-style-span" color="#FF0000">(* Easy; is encoded in the C++ type system. *)</font></font></blockquote><blockquote class="webkit-indent-blockquote" style="margin: 0 0 0 40px; border: none; padding: 0px;"><font class="Apple-style-span" face="Courier">isa<Constant>(x) && isa<Constant>(y)<br></font></blockquote><blockquote class="webkit-indent-blockquote" style="margin: 0 0 0 40px; border: none; padding: 0px;"><font class="Apple-style-span" face="Courier"><font class="Apple-style-span" color="#FF0000">(* Harder; assertions in C++. *)</font></font></blockquote><blockquote class="webkit-indent-blockquote" style="margin: 0 0 0 40px; border: none; padding: 0px;"><font class="Apple-style-span" face="Courier">x->getType() == y->getType()<br></font></blockquote><blockquote class="webkit-indent-blockquote" style="margin: 0 0 0 40px; border: none; padding: 0px;"><span class="Apple-style-span" style="font-family: Courier; ">x->getType()->isIntOrIntVector() || x->getType()->isFPOrFPVector()</span></blockquote><div><div><div><div><div><div><div><div><br class="webkit-block-placeholder"></div><div>I was <i>very</i> impressed that Bryan made <font class="Apple-style-span" face="Courier">build_call</font> statically type check!</div><div><br class="webkit-block-placeholder"></div><div>Still, there are also some problems that I don't think are tractable. Consider <font class="Apple-style-span" face="Courier">param 1 f</font>. Even if the type checker knows the type of <font class="Apple-style-span" face="Courier">f</font> via something like <font class="Apple-style-span" face="Courier">`Function of ('a v -> 'b v -> 'c v)<span class="Apple-style-span" style="font-family: 'Trebuchet MS'; "><font class="Apple-style-span" face="Courier"> v</font>, I don't think it's possible for the expression to have the correct type. Thought it might be possible with <font class="Apple-style-span" face="Courier">param0 f</font>, <font class="Apple-style-span" face="Courier">param1 f</font>, etc. And clearly <font class="Apple-style-span" face="Courier">params f</font> can't have a type significantly more restricted than <font class="Apple-style-span" face="Courier">llvalue v array</font>.</span></font></div><div><br class="webkit-block-placeholder"></div><div><div><div></div></div></div><div>Speaking of which, Bryan, if you're still reading the list, do you have any plans for submitting your Haskell bindings to the project?</div><div><div><br class="webkit-block-placeholder"></div><blockquote type="cite"></blockquote></div><div apple-content-edited="true"><span class="Apple-style-span" style="border-collapse: separate; border-spacing: 0px 0px; color: rgb(0, 0, 0); font-family: Trebuchet MS; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; text-align: auto; -khtml-text-decorations-in-effect: none; text-indent: 0px; -apple-text-size-adjust: auto; text-transform: none; orphans: 2; white-space: normal; widows: 2; word-spacing: 0px; "><div style="word-wrap: break-word; -khtml-nbsp-mode: space; -khtml-line-break: after-white-space; "><span class="Apple-style-span" style="border-collapse: separate; border-spacing: 0px 0px; color: rgb(0, 0, 0); font-family: Trebuchet MS; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; text-align: auto; -khtml-text-decorations-in-effect: none; text-indent: 0px; -apple-text-size-adjust: auto; text-transform: none; orphans: 2; white-space: normal; widows: 2; word-spacing: 0px; "><span class="Apple-style-span" style="border-collapse: separate; border-spacing: 0px 0px; color: rgb(0, 0, 0); font-family: Trebuchet MS; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; text-align: auto; -khtml-text-decorations-in-effect: none; text-indent: 0px; -apple-text-size-adjust: auto; text-transform: none; orphans: 2; white-space: normal; widows: 2; word-spacing: 0px; "><span class="Apple-style-span" style="border-collapse: separate; border-spacing: 0px 0px; color: rgb(0, 0, 0); font-family: Trebuchet MS; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; text-align: auto; -khtml-text-decorations-in-effect: none; text-indent: 0px; -apple-text-size-adjust: auto; text-transform: none; orphans: 2; white-space: normal; widows: 2; word-spacing: 0px; "><span class="Apple-style-span" style="border-collapse: separate; border-spacing: 0px 0px; color: rgb(0, 0, 0); font-family: Trebuchet MS; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; text-align: auto; -khtml-text-decorations-in-effect: none; text-indent: 0px; -apple-text-size-adjust: auto; text-transform: none; orphans: 2; white-space: normal; widows: 2; word-spacing: 0px; "><span class="Apple-style-span" style="border-collapse: separate; border-spacing: 0px 0px; color: rgb(0, 0, 0); font-family: Trebuchet MS; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; text-align: auto; -khtml-text-decorations-in-effect: none; text-indent: 0px; -apple-text-size-adjust: auto; text-transform: none; orphans: 2; white-space: normal; widows: 2; word-spacing: 0px; ">— Gordon<br class="Apple-interchange-newline"></span></span></span></span></span></div></span> </div><br></div></div></div></div></div></div></div></div></body></html>