Proposal: ValidateMonoLiterals - Initial bikeshed discussion

[Merijn Verstraaten]

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 <hesselink at gmail.com> wrote:
> 
> On Fri, Feb 6, 2015 at 2:49 PM, Dominique Devriese
> <dominique.devriese at cs.kuleuven.be> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs

-------------- 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/ghc-devs/attachments/20150206/cfc2c903/attachment.sig>