Proposal: Add inductively-defined Nat to base

Thu Apr 5 17:55:38 UTC 2018

I think the Agda desugaring trick is possible in Haskell currently, using view patterns:

{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeInType          #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE PatternSynonyms     #-}
{-# LANGUAGE ViewPatterns        #-}

{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}

import Data.Kind          (Type)
import Data.Coerce        (coerce)
import Numeric.Natural    (Natural)
import Data.Type.Equality ((:~:)(..),gcastWith)
import Unsafe.Coerce      (unsafeCoerce)

data family The k :: k -> Type

class Sing (a :: k) where sing :: The k (a :: k)

data Nat = Z | S Nat

newtype instance The Nat n = NatSing Natural

instance Sing Z where
    sing = NatSing 0

instance Sing n => Sing (S n) where
    sing =
        (coerce :: (Natural -> Natural) -> (The Nat n -> The Nat (S n)))
            succ sing

data Natty n where
        ZZy :: Natty Z
        SSy :: The Nat n -> Natty (S n)

getNatty :: The Nat n -> Natty n
getNatty (NatSing n :: The Nat n) = case n of
  0 -> gcastWith (unsafeCoerce Refl :: n :~: Z) ZZy
  _ -> gcastWith (unsafeCoerce Refl :: n :~: S m) (SSy (NatSing (pred n)))

pattern Zy :: () => (n ~ Z) => The Nat n
pattern Zy <- (getNatty -> ZZy) where Zy = NatSing 0

pattern Sy :: () => (n ~ S m) => The Nat m -> The Nat n
pattern Sy x <- (getNatty -> SSy x) where Sy (NatSing x) = NatSing (succ x)
{-# COMPLETE Zy, Sy #-}

type family (+) (n :: Nat) (m :: Nat) :: Nat where
        Z + m = m
        S n + m = S (n + m)

-- | Efficient addition, with type-level proof.
add :: The Nat n -> The Nat m -> The Nat (n + m)
add = (coerce :: (Natural -> Natural -> Natural) -> The Nat n -> The Nat m -> The Nat (n + m)) (+)

-- | Proof on efficient representation.
addZeroRight :: The Nat n -> n + Z :~: n
addZeroRight Zy = Refl
addZeroRight (Sy n) = gcastWith (addZeroRight n) Refl

> On 19 Mar 2018, at 12:53, Daniel Cartwright <chessai1996 at gmail.com> wrote:
> 
> Yes, that is along the lines of something I want.
> 
> On Mar 19, 2018 12:13 PM, "Carter Schonwald" <carter.schonwald at gmail.com> wrote:
> what would be nice would be figuring out how to do something like the Agda desugaring trick, where naturals have both the inductive rep exposed AND efficient primops arithmetically 
> 
> On Thu, Mar 15, 2018 at 10:41 PM, Richard Eisenberg <rae at cs.brynmawr.edu> wrote:
> For what it's worth, I'm ambivalent on this one until we have a way to use these Nats without the terrible performance they would naturally have. I'm not against -- this definition would be useful -- but I also don't see such a big advantage to baking these into GHC's shipped libraries.
> 
> Perhaps my hesitation is mostly because I favor a smaller `base`, in general.
> 
> Happy to defer to others here.
> 
> Richard
> 
> 
>> On Mar 15, 2018, at 1:05 PM, Edward Kmett <ekmett at gmail.com> wrote:
>> 
>> Er, by that I mean the type level nats, not the value-level ones.
>> 
>> On Thu, Mar 15, 2018 at 6:05 PM, Edward Kmett <ekmett at gmail.com> wrote:
>> AFAIK, the existing naturals in base don't have any useful internal structure permitting this sort of thing.
>> 
>> -Edward
>> 
>> On Thu, Mar 15, 2018 at 3:48 PM, Carter Schonwald <carter.schonwald at gmail.com> wrote:
>> Could we provide a pattern synonym for treating naturals as in base already as being peano encoded ?
>> 
>> On Wed, Mar 14, 2018 at 11:51 PM Daniel Cartwright <chessai1996 at gmail.com> wrote:
>> I just realised I made a typo. For full clarity, the function 'f' should be:
>> 
>> f : D -> N -> R
>> where
>> D = Data Structure isomorphic to Nat (or any numeric type)
>> N = Number System Encoding
>> R = Representation of the numeric type in N.
>> 
>> For Nats, the simplest example would be:
>> 
>> f : List () -> Binary -> BinaryEncodingOfNat
>> 
>> 
>> On Wed, Mar 14, 2018 at 9:47 PM, Daniel Cartwright <chessai1996 at gmail.com> wrote:
>> I prefer Z and S, but wrote Zero and Succ for clarity (though the likelihood of being at all misunderstood was small).
>> 
>> Most recent definitions I see use Z and S.
>> 
>> On Wed, Mar 14, 2018 at 9:41 PM, David Feuer <david.feuer at gmail.com> wrote:
>> Another problem: different people like to call the constructors by different names. I personally prefer Z and S, because they're short. Some people like Zero and Succ or Suc.
>> 
>> On Mar 14, 2018 9:06 PM, "Daniel Cartwright" <chessai1996 at gmail.com> wrote:
>> The proposed addition is simple, add the following to base:
>> 
>> data Nat = Zero | Succ Nat,
>> 
>> i.e. Peano Nats - commonly used along with -XDataKinds.
>> 
>> I will list the pros/cons I see below:
>> 
>> Pros:
>> - This datatype is commonly defined throughout many packages throughout Hackage. It would be good for it to have a central location
>> - The inductive definition of 'Nat' is useful for correctness (e.g. safeHead :: Vec a (Succ n) -> a; safeHead (Cons a as) = a;)
>> - -XDependentHaskell is likely to bring this into base anyway
>> - I believe that it might be possible to eliminate a Peano Nat at some stage during/after typechecking. I'm not well-versed in GHC implementation, but something along the lines of possibly converting an inductive Nat to a GMP Integer using some sort of specialisation (Succ -> +1)? Another interesting, related approach (and this is a very top-level view, and perhaps not totally sensical) would be something like a function 'f', that given a data structure and a number system, outputs the representation of that data structure in that number system (Nat is isomorphic to List (), so f : List () -> Binary -> BinaryListRep)
>> 
>> Cons:
>> - -XDependentHaskell will most likely obviate any benefit brought about by type families defined in base that directly involve Nat
>> - Looking at base, I'm not sure where this would go. Having it in its own module seems a tad strange.
>> 
>> I am open to criticism concerning the usefulness of the idea, or if anyone sees a Pro(s)/Con(s) that I am missing.
>> 
>> 
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>> 
>> 
>> 
>> 
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>> 
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>> 
>> 
>> 
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> 
> 
> 
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> 
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries