Proposal: ValidateMonoLiterals - Initial bikeshed discussion

[Merijn Verstraaten]

Hi Adam,

> On 6 Feb 2015, at 21:31, Adam Gundry <adam at well-typed.com> wrote:
> What does "all monomorphic cases" mean? Is the idea what GHC
> would typecheck an expression involving a literal integer, determine
> that the occurrence had type Even, then evaluate the TH splice *after*
> typechecking? Whereas if the occurrence had a non-ground type, it would
> do something else?

Yes, Typed TH already runs *after* type checking, which is what allows you to do validation based on the resulting type. The main reason why I was only proposing to do this for monomorphic values is, because, how could you possible validate a polymorphic literal? Which validation function would you use?

You could ban polymorphic literals, but that'd involve eliminating most uses of polymorphic Num functions (as I mentioned as another email), which would break so much code it would render the extension unusable in "real" code. I'm open to better ideas on how to tackle this, the main reason I started this discussion is because I don't really like this "polymorphic literals fail at compile time" thing either. I just don't see how to solve it without going all dependent types on the problem.

> None of this is particularly persuasive, I'm afraid. Is it worthwhile
> introducing something new just to avoid having to write a quasi quote?

Actually, I would be mildly ok with quasi quoters, BUT there currently is no Typed TH quasi quoter (as mentioned on the wiki page), additionally, such a quoter does not have access to Lift instances for all but a handful of datatypes until we have a more comprehensive way to generate Lift instances. I think both of these points are also highly relevant for this dicussion.

> I *am* attracted to the idea of indexed classes in place of IsString/Num
> 
>  class KnownSymbol s => IsIndexedString (a :: *) (s :: Symbol) where
>    fromIndexedString :: a
> 
>  class KnownInteger i => IsIndexedInteger (a :: *) (i :: Integer) where
>     fromIndexedInteger :: a
> These have a smooth upgrade path from the existing class instances via
> 
>    default fromIndexedString :: (KnownSymbol s, IsString a) => a
>    fromIndexedString = fromString (symbolVal (Proxy :: Proxy s))
> 
>    default fromIndexedInteger :: (KnownInteger i, Num a) => a
>    fromIndexedInteger = fromInteger (integerVal (Proxy :: Proxy i))
> 
> and other instances can take advantage of the additional type
> information. perhaps we need to bring Dependent Haskell a bit closer
> before this is justifiable...

The main reason I don't like the "dependent haskell" approach or your approach is how much boiler plate it introduces for beginners. ANYONE knows how to write a "String -> Maybe a" function, I barely know how to use your example and I'm very comfortable with the type families/datakinds stuff, how would "ordinary haskellers" use that?

Not to mention, how would I use your "IsIndexedString" in real code? It seems you'd need at least a FunDep + cumbersome annotation? Not to mention that it still performs the conversion at runtime (I would *much* rather have a Lift based approach that just splices finished conversions into the resulting program.

Cheers,
Merijn
-------------- 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/glasgow-haskell-users/attachments/20150209/904cf930/attachment.sig>