Proposal: ValidateMonoLiterals - Initial bikeshed discussion

[Adam Gundry]

Hi Dominique,

On 06/02/15 12:13, Dominique Devriese wrote:
> 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.

Interestingly, the string version of this would be remarkably similar to
the IV class [1] that came up in the redesign of OverloadedRecordFields:

    class IV (x :: Symbol) a where
      iv :: a

though in this case the plan was to have a special syntax for such
literals (e.g. #x).

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.

Adam

[1]
https://ghc.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields/Redesign#Implicitvalues


-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/