Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

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 wrote:

On Fri, Feb 6, 2015 at 2:49 PM, Dominique Devriese 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@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs