Proposal: ValidateMonoLiterals - Initial bikeshed discussion
Merijn Verstraaten
merijn at inconsistent.nl
Fri Feb 6 15:53:56 UTC 2015
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>
More information about the ghc-devs
mailing list