Proposal: ValidateMonoLiterals - Initial bikeshed discussion
Dominique Devriese
dominique.devriese at cs.kuleuven.be
Fri Feb 6 13:41:30 UTC 2015
Hi Merijn,
2015-02-06 13:45 GMT+01:00 Merijn Verstraaten <merijn at inconsistent.nl>:
> I don't see how that would replace the usecase I describe?
I've written out the Even use case a bit, to hopefully clarify my
suggestion. The code is a bit cumbersome and inefficient because I
can't use GHC type-lits because some type-level primitives seem to be
missing (modulo specifically). Type-level Integers (i.e. a kind with
*negative* numbers and literals) would probably also be required for
an actual solution.
{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, DataKinds,
KindSignatures, ExplicitForAll, PolyKinds, ScopedTypeVariables,
ConstraintKinds, TypeFamilies, GADTs, FlexibleContexts #-}
module ValidateMonoLiterals where
data Nat where
Zero :: Nat
Suc :: Nat -> Nat
class KnownNat (n :: Nat) where
natSing :: forall proxy. proxy n -> Integer
instance KnownNat Zero where natSing _ = 0
instance KnownNat k => KnownNat (Suc k) where natSing _ = natSing
(Proxy :: Proxy k) + 1
data Proxy (t :: k) = Proxy
class HasNatLiteral a (k :: Nat) where
literal :: Proxy k -> a
data Even = Even Integer
class CheckEven (k :: Nat) where
instance CheckEven Zero
instance CheckEven k => CheckEven (Suc (Suc k)) where
instance (KnownNat k, CheckEven k) => HasNatLiteral Even (k :: Nat) where
literal _ = Even (fromInteger (natSing (Proxy :: Proxy k)))
instance (KnownNat k) => HasNatLiteral Integer k where
literal _ = natSing (Proxy :: Proxy k)
four :: HasNatLiteral n (Suc (Suc (Suc (Suc Zero)))) => n
four = literal (Proxy :: Proxy (Suc (Suc (Suc (Suc Zero)))))
three :: HasNatLiteral n (Suc (Suc (Suc Zero))) => n
three = literal (Proxy :: Proxy (Suc (Suc (Suc Zero))))
fourI :: Integer
fourI = four
fourEI :: Even
fourEI = four
-- fails with "No instance for CheckEven (Suc Zero)"
-- threeEI :: Even
-- threeEI = three
> I'll give you a more concrete example from a library I'm working on. I'm working on a Haskell implementation of ZeroMQ, the ZMTP protocol lets sockets be named by a "binary identifier with length <= 255 and NOT starting with a NUL byte". As a programmer using this library I would have to write these socket identifiers in my source code. Now I have four options:
> 1) The library just doesn't validate identifiers to be compatible with the protocol (awful!)
>
> 2) My library produces a runtime error on every single invocation of the program (if it doesn't satisfy the constraints it will never successfully work)
>
> 3) I require a newtype'd input type with a smart constructor, which means the programmer still has to handle the "error" case even though it should never happen for literals written in the source.
>
> 4) Using a trick like what I desribed, the above newtype and smart constructor, and check at compile time that it is correct.
Well, I think my suggestion could be used as another alternative. As I
mentioned, the compiler could translate the literal 42 to an
appropriately typed invocation of HasNatLiteral.literal, so that you
could also just write 42 but get the additional compile-time checking.
> To be honest, I don't even see how your example would generalise to the rather trivial example using Even? For example, suppose we have "foo :: Even -> SomeData" how would I write "foo 2" using your idea in a way that, at compile time, checks that I'm not passing an invalid literal to foo?
See above: the type of foo doesn't change w.r.t. your approach.
> As a further aside, your "type checking remains decidable" comment seems to imply that you think that type checking becomes undecidable with what I propose? Can you explain how that could be, considering that it already works in GHC, albeit in a very cumbersome way?
What I mean is that meta-programs invoked through TH can always fail
to terminate
(even though the ones you are using in your example are terminating).
Consider what happens if you change the definition of your validate to
this (or someone else implements your validateInteger like this for a
type):
validate :: forall a . Validate a => Integer -> Q (TExp a)
validate i = validate (i+1)
Regards,
Dominique
More information about the Glasgow-haskell-users
mailing list