Proposal: ValidateMonoLiterals - Initial bikeshed discussion
Adam Gundry
adam at well-typed.com
Fri Feb 6 13:20:24 UTC 2015
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/
More information about the Glasgow-haskell-users
mailing list