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 :

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 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@haskell.org] On Behalf Of Merijn | Verstraaten | Sent: 05 February 2015 14:46 | To: ghc-devs@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@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Hi Merijn, 2015-02-06 13:45 GMT+01:00 Merijn Verstraaten :

I don't see how that would replace the usecase I describe?

I've written out the Even use case a bit, to hopefully clarify my suggestion. The code is a bit cumbersome and inefficient because I can't use GHC type-lits because some type-level primitives seem to be missing (modulo specifically). Type-level Integers (i.e. a kind with *negative* numbers and literals) would probably also be required for an actual solution. {-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, DataKinds, KindSignatures, ExplicitForAll, PolyKinds, ScopedTypeVariables, ConstraintKinds, TypeFamilies, GADTs, FlexibleContexts #-} module ValidateMonoLiterals where data Nat where Zero :: Nat Suc :: Nat -> Nat class KnownNat (n :: Nat) where natSing :: forall proxy. proxy n -> Integer instance KnownNat Zero where natSing _ = 0 instance KnownNat k => KnownNat (Suc k) where natSing _ = natSing (Proxy :: Proxy k) + 1 data Proxy (t :: k) = Proxy class HasNatLiteral a (k :: Nat) where literal :: Proxy k -> a data Even = Even Integer class CheckEven (k :: Nat) where instance CheckEven Zero instance CheckEven k => CheckEven (Suc (Suc k)) where instance (KnownNat k, CheckEven k) => HasNatLiteral Even (k :: Nat) where literal _ = Even (fromInteger (natSing (Proxy :: Proxy k))) instance (KnownNat k) => HasNatLiteral Integer k where literal _ = natSing (Proxy :: Proxy k) four :: HasNatLiteral n (Suc (Suc (Suc (Suc Zero)))) => n four = literal (Proxy :: Proxy (Suc (Suc (Suc (Suc Zero))))) three :: HasNatLiteral n (Suc (Suc (Suc Zero))) => n three = literal (Proxy :: Proxy (Suc (Suc (Suc Zero)))) fourI :: Integer fourI = four fourEI :: Even fourEI = four -- fails with "No instance for CheckEven (Suc Zero)" -- threeEI :: Even -- threeEI = three

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.

Well, I think my suggestion could be used as another alternative. As I mentioned, the compiler could translate the literal 42 to an appropriately typed invocation of HasNatLiteral.literal, so that you could also just write 42 but get the additional compile-time checking.

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?

See above: the type of foo doesn't change w.r.t. your approach.

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?

What I mean is that meta-programs invoked through TH can always fail to terminate (even though the ones you are using in your example are terminating). Consider what happens if you change the definition of your validate to this (or someone else implements your validateInteger like this for a type): validate :: forall a . Validate a => Integer -> Q (TExp a) validate i = validate (i+1) Regards, Dominique

2015-02-06 14:20 GMT+01:00 Adam Gundry :

It seems to me that what you would describe would work, and the avoidance of TH is a merit, but the downside is the complexity of implementing even relatively simple validation at the type level (as opposed to just reusing a term-level function). For Merijn's Even example I guess one could do something like this in current GHC:

type family IsEven (n :: Nat) :: Bool where IsEven 0 = True IsEven 1 = False IsEven n = n - 2

instance (KnownNat n, IsEven n ~ True) => HasIntegerLiteral Even n where literal = Even (natVal (Proxy :: Proxy n))

but anything interesting to do with strings (e.g. checking that ByteStrings are ASCII) is rather out of reach at present.

Agreed. For the idea to scale, good support for type-level programming with Integers/Strings/... is essential. Something else that would be useful is an unsatisfiable primitive constraint constructor `UnsatisfiableConstraint :: String -> Constraint` that can be used to generate custom error messages. Then one could write something like type family MustBeTrue (t :: Bool) (error :: String) :: Constraint type family MustBeTrue True _ = () type family MustBeTrue False error = UnsatisfiableConstraint error type family MustBeEven (n :: Nat) :: Constraint type family MustBeEven n = MustBeTrue (IsEven n) ("Error in Even literal :'" ++ show n ++ "' is not even!") instance (KnownNat n, MustBeEven n) => HasIntegerLiteral Even n where ... Regards, Dominique

While I am certainly in favour of better and more flexible approaches to enforcing this in the type system (I'm a big fan of all the dependent Haskell/singletons stuff), I don't think this is an appropriate solution here. First off, a lot of interesting and important cases can't feasibly be solved right now (i.e., most things involving strings/lists). More importantly, I think the examples given in this thread so far are FAR beyond the capabilities of beginner/intermediate haskellers, whereas implementing a terminating "String -> Maybe a" is fairly trivial. So in terms of pragmatical usability I think the TH approach is easier to implement in GHC, easier to use by end users and more flexible and powerful than the suggested type families/DataKinds. I'm all in favour of some of the below directions, but pragmatically I think it'll be a while before any of those problems are usable by any beginners. I also realise a lot of people prefer avoiding TH if at all possible, but given that this is an extension that people have to opt into that won't otherwise affect their code, I think that's acceptable. Personally, I'd gladly use TH in exchange for this sort of checking and I've talked to several others that would to. Cheers, Merijn

On 6 Feb 2015, at 14:55, Erik Hesselink wrote:

On Fri, Feb 6, 2015 at 2:49 PM, Dominique Devriese wrote:

...

Agreed. For the idea to scale, good support for type-level programming with Integers/Strings/... is essential. Something else that would be useful is an unsatisfiable primitive constraint constructor `UnsatisfiableConstraint :: String -> Constraint` that can be used to generate custom error messages. Then one could write something like

type family MustBeTrue (t :: Bool) (error :: String) :: Constraint type family MustBeTrue True _ = () type family MustBeTrue False error = UnsatisfiableConstraint error

type family MustBeEven (n :: Nat) :: Constraint type family MustBeEven n = MustBeTrue (IsEven n) ("Error in Even literal :'" ++ show n ++ "' is not even!")

instance (KnownNat n, MustBeEven n) => HasIntegerLiteral Even n where ...

Note that there is a trick to fake this with current GHC: you can write an equality constraint that is false, involving the type level string:

...

type family MustBeTrue False error = (() ~ error)

Erik _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs