Proposal: Add inductively-defined Nat to base

[Daniel Cartwright]

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.

[Daniel Cartwright]

I believe that at the value level, Peano Nats can be optimised using
pattern synonyms. The primary interest of Peano Nats, however, is in their
use at the kind level - so I think two things are possible:

1. With -XDependentHaskell, one can define a pattern synonym allowing the
optimisation of Peano Nats,
2. With type families, it _might_ be possible to define a weaker form of
(1), provided it is possible to put a type synonym on the LHS
of a type family.

Question: Can a TypeApplication be used on the LHS of an injective type
family?

Post by Daniel Cartwright
data Nat = Zero | Succ Nat,
i.e. Peano Nats - commonly used along with -XDataKinds.
- 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)
- -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.

[David Feuer]

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" <***@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.

[Daniel Cartwright]

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.

Post by David Feuer
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.
data Nat = Zero | Succ Nat,
i.e. Peano Nats - commonly used along with -XDataKinds.
- 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)
- -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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Daniel Cartwright]

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

Post by Daniel Cartwright
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.

Post by David Feuer
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.
data Nat = Zero | Succ Nat,
i.e. Peano Nats - commonly used along with -XDataKinds.
- 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)
- -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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Carter Schonwald]

Could we provide a pattern synonym for treating naturals as in base already
as being peano encoded ?

Post by Daniel Cartwright
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.
f : List () -> Binary -> BinaryEncodingOfNat

Post by Daniel Cartwright
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.

Post by David Feuer
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.
data Nat = Zero | Succ Nat,
i.e. Peano Nats - commonly used along with -XDataKinds.
- 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)
- -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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Edward Kmett]

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 <

Post by Carter Schonwald
Could we provide a pattern synonym for treating naturals as in base
already as being peano encoded ?

Post by Daniel Cartwright
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.
f : List () -> Binary -> BinaryEncodingOfNat

Post by Daniel Cartwright
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.

Post by David Feuer
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.
data Nat = Zero | Succ Nat,
i.e. Peano Nats - commonly used along with -XDataKinds.
- 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)
- -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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Edward Kmett]

Er, by that I mean the type level nats, not the value-level ones.

Post by Edward Kmett
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 <

Post by Carter Schonwald
Could we provide a pattern synonym for treating naturals as in base
already as being peano encoded ?

Post by Daniel Cartwright
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.
f : List () -> Binary -> BinaryEncodingOfNat
On Wed, Mar 14, 2018 at 9:47 PM, Daniel Cartwright <

Post by Daniel Cartwright
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.

Post by David Feuer
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.
data Nat = Zero | Succ Nat,
i.e. Peano Nats - commonly used along with -XDataKinds.
- 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)
- -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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Richard Eisenberg]

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

Post by Edward Kmett
Er, by that I mean the type level nats, not the value-level ones.
AFAIK, the existing naturals in base don't have any useful internal structure permitting this sort of thing.
-Edward
Could we provide a pattern synonym for treating naturals as in base already as being peano encoded ?
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.
f : List () -> Binary -> BinaryEncodingOfNat
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.
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.
data Nat = Zero | Succ Nat,
i.e. Peano Nats - commonly used along with -XDataKinds.
- 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)
- -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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Carter Schonwald]

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

Post by Richard Eisenberg
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
Er, by that I mean the type level nats, not the value-level ones.

Post by Edward Kmett
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 <

Post by Carter Schonwald
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 <

Post by Daniel Cartwright
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.
f : List () -> Binary -> BinaryEncodingOfNat
On Wed, Mar 14, 2018 at 9:47 PM, Daniel Cartwright <

Post by Daniel Cartwright
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.

Post by David Feuer
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.
data Nat = Zero | Succ Nat,
i.e. Peano Nats - commonly used along with -XDataKinds.
- 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)
- -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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Daniel Cartwright]

Yes, that is along the lines of something I want.

Post by Carter Schonwald
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

Post by Richard Eisenberg
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
Er, by that I mean the type level nats, not the value-level ones.

Post by Edward Kmett
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 <

Post by Carter Schonwald
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 <

Post by Daniel Cartwright
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.
f : List () -> Binary -> BinaryEncodingOfNat
On Wed, Mar 14, 2018 at 9:47 PM, Daniel Cartwright <

Post by Daniel Cartwright
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.

Post by David Feuer
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.
data Nat = Zero | Succ Nat,
i.e. Peano Nats - commonly used along with -XDataKinds.
- 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)
- -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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Donnacha Oisín Kidney]

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

Post by Daniel Cartwright
Yes, that is along the lines of something I want.
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
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

Post by Edward Kmett
Er, by that I mean the type level nats, not the value-level ones.
AFAIK, the existing naturals in base don't have any useful internal structure permitting this sort of thing.
-Edward
Could we provide a pattern synonym for treating naturals as in base already as being peano encoded ?
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.
f : List () -> Binary -> BinaryEncodingOfNat
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.
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.
data Nat = Zero | Succ Nat,
i.e. Peano Nats - commonly used along with -XDataKinds.
- 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)
- -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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Jon Purdy]

One thing I like about the naturals with the “linked list” representation
is that they’re lazy. When I was first learning Haskell, years ago, I
expected something like “length xs > 1” to only evaluate “xs” up to the
second constructor—that doesn’t work with “length” and “Int”, being strict,
but it does work with “genericLength” and a lazy “Nat” (and “Ord” instance
I guess).

So I think it would be desirable for an optimised representation to
preserve this, but I dunno if it’s possible/easy, or if anyone else
particularly cares—the use cases I know of are admittedly narrow, but the
fault might just be in my knowledge. I suppose there could be lazy and
strict versions of the “Nat” type if it seems important enough.

Post by Donnacha Oisín Kidney
{-# 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

Post by Daniel Cartwright
Yes, that is along the lines of something I want.
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

Post by Daniel Cartwright
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.

Post by Daniel Cartwright
Perhaps my hesitation is mostly because I favor a smaller `base`, in

general.

Post by Daniel Cartwright
Happy to defer to others here.
Richard

Post by Edward Kmett
Er, by that I mean the type level nats, not the value-level ones.
AFAIK, the existing naturals in base don't have any useful internal

structure permitting this sort of thing.

Post by Daniel Cartwright

Post by Edward Kmett
-Edward
On Thu, Mar 15, 2018 at 3:48 PM, Carter Schonwald <
Could we provide a pattern synonym for treating naturals as in base

already as being peano encoded ?

Post by Daniel Cartwright

Post by Edward Kmett
On Wed, Mar 14, 2018 at 11:51 PM Daniel Cartwright <
I just realised I made a typo. For full clarity, the function 'f'
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.
f : List () -> Binary -> BinaryEncodingOfNat
On Wed, Mar 14, 2018 at 9:47 PM, Daniel Cartwright <
I prefer Z and S, but wrote Zero and Succ for clarity (though the

likelihood of being at all misunderstood was small).

Post by Daniel Cartwright

Post by Edward Kmett
Most recent definitions I see use Z and S.
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.

Post by Daniel Cartwright

Post by Edward Kmett
data Nat = Zero | Succ Nat,
i.e. Peano Nats - commonly used along with -XDataKinds.
- This datatype is commonly defined throughout many packages throughout

Hackage. It would be good for it to have a central location

Post by Daniel Cartwright

Post by Edward Kmett
- The inductive definition of 'Nat' is useful for correctness (e.g.

safeHead :: Vec a (Succ n) -> a; safeHead (Cons a as) = a;)

Post by Daniel Cartwright

Post by Edward Kmett
- -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)

Post by Daniel Cartwright

Post by Edward Kmett
- -XDependentHaskell will most likely obviate any benefit brought about

by type families defined in base that directly involve Nat

Post by Daniel Cartwright

Post by Edward Kmett
- Looking at base, I'm not sure where this would go. Having it in its

own module seems a tad strange.

Post by Daniel Cartwright

Post by Edward Kmett
I am open to criticism concerning the usefulness of the idea, or if

anyone sees a Pro(s)/Con(s) that I am missing.

Post by Daniel Cartwright

Post by Edward Kmett
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Henning Thielemann]

One thing I like about the naturals with the “linked list” representation is that they’re lazy. When I was first
learning Haskell, years ago, I expected something like “length xs > 1” to only evaluate “xs” up to the second
constructor—that doesn’t work with “length” and “Int”, being strict, but it does work with “genericLength” and a
lazy “Nat” (and “Ord” instance I guess).

It would also work with:
void xs > replicate 1 ()

[Donnacha Oisín Kidney]

This solution would still keep the lazy Nat type around: the optimised version (the patterns Sy and Zy over the newtype for Natural) is just a singleton, for proofs.

You don’t get the benefit of laziness for proofs, regardless (as you have to pattern match to prove), so I don’t think you lose anything with this representation.

What I had in mind for it was something like this:

data Tree n a where
Leaf :: Tree Z a
Node :: The Nat n -> a -> Tree n a -> Tree m a -> Tree (S (n + m)) a

where the singleton could be efficiently compared and added, but also would provide a proof. Again, I don’t think laziness can be of benefit here.

One thing I like about the naturals with the “linked list” representation is that they’re lazy. When I was first
learning Haskell, years ago, I expected something like “length xs > 1” to only evaluate “xs” up to the second
constructor—that doesn’t work with “length” and “Int”, being strict, but it does work with “genericLength” and a
lazy “Nat” (and “Ord” instance I guess).

void xs > replicate 1 ()_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries