[TypeApplications] Create Proxy-free alternatives of functions in base

[Iceland_jack]

Now that we have ​TypeApplications how about we create a Proxy-free version of functions in base that currently require it:

tr :: forall a. Typeable a => TypeRep
tr = typeRep @Proxy @a Proxy

symbol :: forall s. KnownSymbol s => String
symbol = symbolVal @s Proxy

nat :: forall n. KnownNat n => Integer
nat = natVal @n Proxy

While we're at it let's use ​Natural as the value-level representation of Nat, avoiding Maybe in someNatVal :: Integer -> Maybe SomeNat:

nat :: forall n. KnownNat n => Natural
nat = natVal @n Proxy

someNatVal :: Natural -> SomeNat
someNatVal = ...

[rwbarton]

sizeof and other Storable methods come to mind too.

[simonpj]

I'm all for it. Doubtless thinking of suitable names will be the most awkward bit.

[ekmett]

I'm likewise in favor, so long as these are new combinators and we don't go and kill all the existing combinators.

[Iceland_jack]

To get the ball rolling I suggest prefixing them with {in?,}definite articles:

  aNat :: forall n. KnownNat n => Natural
theNat :: forall n. KnownNat n => Natural

  aSymbol :: forall s. KnownSymbol s => String
theSymbol :: forall s. KnownSymbol s => String

  aTypeRep :: forall t. Typeable t => TypeRep
theTypeRep :: forall t. Typeable t => TypeRep

theSizeOf :: forall s. Storable s => Int
theSizeOf = sizeOf @s undefined

For the Tangent of the Day (as a Service) (TotD(aaS)), how should the inclusion of Natural in base influence functions and other libraries?

Functions like length, take, drop, splitAt, replicate scream for natural numbers as their arguments: Their types are of course well established, Int is also fixed- while Natural is arbitrary-precision. Is Word suitable? Maybe not worth it.

Lens defines instance FunctorWithIndex Int [] whose functional dependency forbids the index of lists from being (the arguably more ‘natural’) Natural or Word. Changing them retroactively is a pain but would it make sense in a perfect world?

Edit: Alternative proposals: zeTypeRep, daRealSizeOf

[rwbarton]

Replying to Iceland_jack:

For the Tangent of the Day (as a Service) (TotD(aaS)), how should the inclusion of Natural in base influence functions and other libraries?

Off-topic, but...

Functions like length, take, drop, splitAt, replicate scream for natural numbers as their arguments: Their types are of course well established, Int is also fixed- while Natural is arbitrary-precision. Is Word suitable? Maybe not worth it.

Very unsuitable as long as subtraction on Word has wrap-around behavior rather than erroring. You would fail to catch a lot of programming errors that way, when passing wrapped values to functions that used to check whether their argument was negative, and in other cases you would silently change program behavior, when using functions that used to treat negative values as 0. See ​http://www.wabbo.org/blog/2014/22aug_on_bananas.html for a related example from Rust.

Word is basically useless as an "efficient small-ish Natural" for this reason, and only makes sense when you specifically want the machine-specific wrap-around behavior, or when doing bit manipulation only. (And yes, Int can overflow too, making it somewhat less effective as an "efficient small-ish Integer", but overflowing an Int computation requires large inputs (which are often impossible to provide to the program in practice), while a Word computation can be overflowed with very small inputs.)

[Iceland_jack]

Replying to rwbarton:

Word is basically useless as an "efficient small-ish Natural" for this reason, and only makes sense when you specifically want the machine-specific wrap-around behavior, or when doing bit manipulation only.

A fixed-precision type with the underflow semantics of Natural could be useful. Anyway </offtopic>

[goldfire]

Might I suggest that we experiment with this outside of base for a bit? TypeApplications is awfully new. I honestly don't think it will, but it might well change. Given the very loud grumbling we've all heard about changes to base, I think it would be prudent to make a proxyfree-base that users can opt into. If all goes well, I think merging into base somehow is great. But maybe for 8.2.

[ekmett]

Using unsigned types for size and having random wraparound issues is a huge source of user error in the C++ world, to the point where it is arguably a worse problem than dealing with negative values, since there it is an easy check. On the other hand using a type with undefined overflow once you start dealing with arithmetic and have x + y - z situations the logic gets rather complicated and very branchy. The number of branches involved gets even sillier if that type is actually a Natural and it has to deal with both small and large code paths behind the scenes. Using Natural there would turn such code from two assembly operations and an optional bounds check to something involving up to 16 cases which can't be avoided without getting too clever about it.

Like it or not Int took on the role of sizes in the Haskell community, and it pushes the bad corner cases far away from the domain of actual use as noted by Reid. I don't see that changing in the foreseeable future. I think I'm going to echo Richard's suggestion of doing this "outside base", but without the positive outlook about it being merged back.

Switching KnownNat to Natural and the like is on the agenda, however.

[RyanGlScott]

Replying to goldfire:

Might I suggest that we experiment with this outside of base for a bit? TypeApplications is awfully new. I honestly don't think it will, but it might well change. Given the very loud grumbling we've all heard about changes to base, I think it would be prudent to make a proxyfree-base that users can opt into. If all goes well, I think merging into base somehow is great. But maybe for 8.2.

Coincidentally, I just started a ​proxied library to retrofit functions like sizeOf to take a Proxy as an argument. I'd be eager to add a Data.Proxyless module to proxied that gives the corresponding Proxy-free equivalent functions that leverage TypeApplications. (The name proxied then becomes kind of a misnomer, but at the end of the day it'd accomplish what this ticket sets out to do.)