Proposal: ValidateMonoLiterals - Initial bikeshed discussion

[Dominique Devriese]

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