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/ _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users