[Ur] More questions

Adam Chlipala adamc at impredicative.com
Sun Dec 12 19:33:11 EST 2010


Marc Weber wrote:
> So would you mind running the same test on your machine?

First, I ran the test using [List.app] instead of [List.mapM] and it 
worked fine, so this is the solution, for all practical purposes. :)

Second, I reproduced your bug, and I think I've isolated it to what 
looks like a bug in GCC, related to use of a GCC C extension.  Would 
anyone mind sanity-checking this relatively-minimized source file for me?
     http://adam.chlipala.net/tmp/test.c
With my GCC (and presumably with Marc's, too), it prints only one line 
of output, though I was expecting two.  It seems GCC is dropping certain 
side effects that occur inside struct initializers in certain contexts.  
That is the root cause of the dropped SQL side effects from the larger 
example.

>> BTW, you could write [TRUE] instead of [1 = 1].  IMO, it's slightly
>> nicer looking.
>>      
> I'd say ur could support DELETE without dummy where. That would be even
> prettier :)
>    

My reasoning here was that it would be way too easy to accidentally 
delete all rows from a table.  The need to include an explicit 'WHERE' 
clause is a kind of "are you sure?" prompt.

> I tried asking: Why
> is this line necessary. I would have no chance coming up with that line
> myself. Shouldn't the information whether a key is nullable be encoded
> in the type ?
>
> The code looks like this:
>
>      functor Make(M : sig
>                       type key
>                       [...]
>                       val key_inj : sql_injectable_prim key
>    

The input [key_inj] doesn't have to do with nullability.  Rather, this 
value proves that the type [key] is one that the SQL engine 
understands.  Because of this, you couldn't get away with asking the 
functor to use key types like [int -> int], [list int], etc..  You can 
only use key types that you can prove are SQL-compatible.



More information about the Ur mailing list