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 <hessel...@gmail.com> wrote:
>
> On Fri, Feb 6, 2015 at 2:49 PM, Dominique Devriese
> <dominique.devri...@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-d...@haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
