Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Fri Feb 6 12:45:40 UTC 2015

Hi Dominique,

I don't see how that would replace the usecase I describe? I'll give you a more concrete example from a library I'm working on. I'm working on a Haskell implementation of ZeroMQ, the ZMTP protocol lets sockets be named by a "binary identifier with length <= 255 and NOT starting with a NUL byte". As a programmer using this library I would have to write these socket identifiers in my source code. Now I have four options:

1) The library just doesn't validate identifiers to be compatible with the protocol (awful!)

2) My library produces a runtime error on every single invocation of the program (if it doesn't satisfy the constraints it will never successfully work)

3) I require a newtype'd input type with a smart constructor, which means the programmer still has to handle the "error" case even though it should never happen for literals written in the source.

4) Using a trick like what I desribed, the above newtype and smart constructor, and check at compile time that it is correct.

To be honest, I don't even see how your example would generalise to the rather trivial example using Even? For example, suppose we have "foo :: Even -> SomeData" how would I write "foo 2" using your idea in a way that, at compile time, checks that I'm not passing an invalid literal to foo?

As a further aside, your "type checking remains decidable" comment seems to imply that you think that type checking becomes undecidable with what I propose? Can you explain how that could be, considering that it already works in GHC, albeit in a very cumbersome way?

As for working with Safe Haskell, I'm all for better Safe Haskell support in TH, but unfortunately I'm already worried about my ability to tackle this proposal, let alone something more ambitious like making TH work better with Safe Haskell, I'll leave that task for someone more familiar with GHC.

Cheers,
Merijn

> On 6 Feb 2015, at 13:13, Dominique Devriese <dominique.devriese at cs.kuleuven.be> wrote:
> 
> Merijn,
> 
> Perhaps only for the sake of discussion: have you considered doing
> something at the type-level instead of using TH? I mean that you could
> change the type of 42 from `forall a. Num a => a` to `forall a.
> HasIntLiteral a '42 => a` where HasIntegerLiteral is a type class of
> kind `* -> 'Integer -> Constraint` and people can instantiate it for
> their types:
> 
> class HasIntegerLiteral (a :: *) (k :: 'Integer) where
>  literal :: a
> 
> The desugarer could then just generate an invocation of "literal".
> 
> An advantage would be that you don't need TH (although you do need
> DataKinds and type-level computation).  Specifically, type-checking
> remains decidable and you can do it in safe haskell and so on.  I
> haven't thought this through very far, so there may be other
> advantages/disadvantages/glaring-holes-in-the-idea that I'm missing.
> 
> Regards,
> Dominique
> 
> 2015-02-06 11:07 GMT+01:00 Merijn Verstraaten <merijn at inconsistent.nl>:
>> And no one of my proofreaders noticed that >.>
>> 
>> I would propose to have the extension replace the 'fromString "foo"', 'fromIntegral 5' and 'fromList [1,2,3]' calls (for monomorphic cases) in the AST with the relevant Typed TH splice.
>> 
>> I considered quasi-quotation initially too, but there's no quasi quotation syntax for Typed TH. I'm guessing that's just an oversight, but I'd really be in favour of adding a typed quasiquoter too. Similarly to thinking we should have an easier way to obtain Lift  instances since, to me at least, it seems that the Lift instance for most ADTs should be fairly trivial?
>> 
>> I'll quickly clarify the proposal on the wiki :)
>> 
>> Cheers,
>> Merijn
>> 
>>> On 5 Feb 2015, at 22:48, Simon Peyton Jones <simonpj at microsoft.com> wrote:
>>> 
>>> I'm all for it.  Syntax sounds like the main difficulty.  Today you could use quasiquotatoin
>>>      [even| 38 |]
>>> and get the same effect as $$(validate 38).  But it's still noisy.
>>> 
>>> So: what is the non-noisy scheme you want to propose?  You don't quite get to that in the wiki page!
>>> 
>>> Simon
>>> 
>>> | -----Original Message-----
>>> | From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Merijn
>>> | Verstraaten
>>> | Sent: 05 February 2015 14:46
>>> | To: ghc-devs at haskell.org; GHC users
>>> | Subject: Proposal: ValidateMonoLiterals - Initial bikeshed discussion
>>> |
>>> | I've been repeatedly running into problems with overloaded literals and
>>> | partial conversion functions, so I wrote up an initial proposal
>>> | (https://ghc.haskell.org/trac/ghc/wiki/ValidateMonoLiterals) and I'd like
>>> | to commence with the bikeshedding and hearing other opinions :)
>>> |
>>> | Cheers,
>>> | Merijn
>> 
>> 
>> _______________________________________________
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users at haskell.org
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 842 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20150206/b8cdfb68/attachment.sig>