Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Fri Feb 6 22:16:33 UTC 2015

Its worth pointing out that when / if luites out of process TH design
happens for ghc, TH will be usable in cross compile builds of ghc as well.
So we shouldn't let that constraint we have for now dictate future tooling
ideas.
On Feb 6, 2015 3:50 PM, "Evan Laforge" <qdunkan at gmail.com> wrote:

> Would it be feasible to make a lighter-weight mode for quasiquotes
> that doesn't require the whole "load the module in ghci" runaround?
> If it didn't need to do that, there wouldn't be much downside to
> turning it on everywhere.  And it would enable lots of QQ conveniences
> that at least I don't think its worth enabling TH for, due to the ghci
> hassle.
>
> Greg Weber recently asked for input on the idea of restricted TH
> modes, this seems related.
>
> If a splice was pure and had no non-Prelude dependencies, could it be
> run without ghci loading and stage restrictions?
>
> I think it's really awkward how numeric literals use fromInteger and
> fromRational, and those functions are grouped into Num and Fractional.
> So if you want to use (+), you also have to accept literals, which
> means you have to accept anything anyone might type.  Has there been
> any kind of proposal to split fromInteger and fromRational into their
> own typeclasses analogous to IsString?
>
> On Fri, Feb 6, 2015 at 9:24 AM, Dan Doel <dan.doel at gmail.com> wrote:
> > Assuming a separate syntax, I believe that the criterion would be as
> simple
> > as ensuring that no ValidateFoo constraints are left outstanding. The
> syntax
> > would add the relevant validate call, and type variables involved in a
> > ValidateFoo constraint would not be generalizable, and would have to be
> > defaulted or inferred from elsewhere, similar to the monomorphism
> > restriction. I'm not sure how difficult that would be to implement.
> >
> > I'm not terribly gung ho on this, though. It feels very ad hoc. Making
> > validation vs. non-validation syntactic rather than just based on
> > polymorphism seems somewhat less so, though; so I'd prefer that
> direction.
> > Finding unused syntax is always a problem, of course.
> >
> > On Fri, Feb 6, 2015 at 11:38 AM, Ryan Trinkle <ryan.trinkle at gmail.com>
> > wrote:
> >>
> >> My greatest concern here would be that, as an application is
> maintained, a
> >> literal might go from monomorphic to polymorphic, or vice versa, without
> >> anybody noticing.  It sounds like this could result in a value silently
> >> becoming partial, which would be a big problem for application
> stability; in
> >> the opposite case - a partial value becoming a compile-time error - I am
> >> somewhat less concerned, but it could still be confusing and disruptive.
> >>
> >> I would prefer that there be some syntactic indication that I want my
> >> literal to be checked at compile time.  This syntax could also add
> whatever
> >> monomorphism requirement is needed, and then it would become a
> compile-time
> >> error for the value to become polymorphic.  I don't know nearly enough
> about
> >> the type system to know whether this is possible.
> >>
> >> Also, it seems to me that it might not be so clean as "monomorphic"
> versus
> >> "polymorphic".  For example, suppose I have this:
> >>
> >> newtype PostgresTableName s = PostgresTableName String
> >>
> >> where 's' is a phantom type representing the DB schema that the name
> lives
> >> in.  The validation function is independent of the schema - it simply
> fails
> >> if there are illegal characters in the name, or if the name is too long.
> >> So, ideally, ("foo\0bar" :: forall s. PostgresTableName s) would fail at
> >> compile time, despite being polymorphic.
> >>
> >>
> >> Ryan
> >>
> >> On Fri, Feb 6, 2015 at 11:16 AM, Merijn Verstraaten
> >> <merijn at inconsistent.nl> wrote:
> >>>
> >>> Ryan,
> >>>
> >>> Unfortunately, yes, you are understanding that correctly.
> >>>
> >>> The reason I qualified it with "monomorphic only" is that, I want to
> >>> avoid breakage that would render the extension practically unusable in
> real
> >>> code.
> >>>
> >>> Let's say I right now have:
> >>>
> >>> foo :: Num a => [a] -> [a]
> >>> foo = map (+1)
> >>>
> >>> I have two options 1) we compile this as currently using fromIntegral
> and
> >>> it WILL break for Even or 2) we reject any polymorphic use of literals
> like
> >>> this. Given the amount of numerical code relying on the polymorphism
> of Num,
> >>> I think the option of not being able to compile Num polymorphic code is
> >>> completely out of the question. Almost no application  would work.
> >>>
> >>> I would advocate in favour of not requiring an IsList/IsString instance
> >>> for the validation class, this would allow you to write a conversion
> that
> >>> ONLY converts literals in a validated way and will never successfully
> >>> convert literals without the extension, since with the extension
> disabled
> >>> GHC would try to use the fromList/fromString from the IsString/IsList
> >>> classes which do not exist.
> >>>
> >>> Unfortunately, given how deeply fromIntegral is tied to the Num class I
> >>> don't see any way to achieve the same for Num. The only option would
> be to
> >>> not make Even an instance of Num, that way the same trick as above
> could
> >>> work. Removing fromIntegral from Num is obviously not going to happen
> and
> >>> without doing that I don't see how we could prevent someone using
> >>> fromIntegral manually to convert to Even in a way that won't break Num
> >>> polymorphic functions. If you have any ideas on how to tackle this,
> I'm all
> >>> open to hearing them!
> >>>
> >>> I agree with you that this is ugly, but I console myself with the
> thought
> >>> that being able to check all monomorphic literals is already a drastic
> >>> improvement over the current state. And in the case of lists and
> strings we
> >>> could actually ensure that things work well, since almost no one writes
> >>> "IsString polymorphic" code.
> >>>
> >>> Cheers,
> >>> Merijn
> >>>
> >>> > On 6 Feb 2015, at 16:59, Ryan Trinkle <ryan.trinkle at gmail.com>
> wrote:
> >>> >
> >>> > I think the idea of compile-time validation for overloaded literals
> is
> >>> > fantastic, and doing it with nicer syntax than quasiquoting would
> really
> >>> > improve things.  However, I'm a bit confused about specifically how
> the
> >>> > requirement that it be monomorphic will play into this.  For
> example, if I
> >>> > have:
> >>> >
> >>> > x = 1
> >>> >
> >>> > Presumably this will compile, and give a run-time error if I ever
> >>> > instantiate its type to Even.  However, if I have:
> >>> >
> >>> > x :: Even
> >>> > x = 1
> >>> >
> >>> > it will fail to compile?  Furthermore, if I have the former, and type
> >>> > inference determines that its type is Even, it sounds like that will
> also
> >>> > fail to compile, but if type inference determines that its type is
> forall a.
> >>> > Nat a => a, then it will successfully compile and then fail at
> runtime.
> >>> >
> >>> > Am I understanding this correctly?
> >>> >
> >>> >
> >>> > Ryan
> >>> >
> >>> > On Fri, Feb 6, 2015 at 8:55 AM, 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
> >>> > _______________________________________________
> >>> > Glasgow-haskell-users mailing list
> >>> > Glasgow-haskell-users at haskell.org
> >>> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> >>>
> >>> _______________________________________________
> >>> Glasgow-haskell-users mailing list
> >>> Glasgow-haskell-users at haskell.org
> >>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> >>>
> >>
> >>
> >> _______________________________________________
> >> Glasgow-haskell-users mailing list
> >> Glasgow-haskell-users at haskell.org
> >> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> >>
> >
> >
> > _______________________________________________
> > Glasgow-haskell-users mailing list
> > Glasgow-haskell-users at haskell.org
> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> >
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20150206/77ca5f16/attachment-0001.html>