SProxy in purescript?

What's the use of Sproxy in purescript?

In Pursuit, it's written as

data SProxy (sym :: Symbol)
--| A value-level proxy for a type-level symbol.

and what is meant by Symbol in purescipt?

First, please note that PureScript now has polykinds since version 0.14 and most functions now use Proxy instead of SProxy. Proxy is basically a generalisation of SProxy.

About Symbols and Strings

PureScript knows value level strings (known as String) and type level strings (known as Symbol).

• A String can have any string value at runtime. The compiler does not track the value of the string.
• A Symbol is different, it can only have one value (but remember, it is on the type level). The compiler keeps track of this string. This allows the compiler to type check certain expressions.

Symbols in Practice

The most prominent use of Symbols is in records. The difference between a Record and a String-Map is that the compiler knows about the keys at compile time and can typecheck lookups.

Now, sometimes we need to bridge the gap between these two worlds: The type level and the value level world. Maybe you know that PureScript records are implemented as JavaScript objects in the official compiler. This means we need to somehow receive a string value from our symbol. The magical function reflectSymbol allows us to turn a symbol into a string. But a symbol is on the type level. This means we can only write a symbol where we can write types (so for example in type definition after ::). This is where the Proxy hack comes in. The SProxy is a simple value that "stores" the type by applying it.

For example the get function from purescript-records allows us to get a value at a property from a record.

get :: forall proxy r r' l a. IsSymbol l => Cons l a r' r => proxy l -> Record r -> a

If we apply the first paramerter we get:

get (Proxy :: Proxy "x") :: forall r a. { x :: a | r } -> a

Now you could argue that you can get the same function by simply writing:

_.x :: forall r a. { x :: a | r } -> a

It has exactly the same type. This leads to one last question:

But why?

Well, there are certain meta programming szenarios, where you don't programm for a specific symbol, but rather for any symbol. Imagine you want to write a JSON serialiser for any record. You might want to "iterate" over every property of the record, get the value, turn the value itself into JSON and then concatinate the key value pair with all the other keys and values.

An example for such an implementation can be found here

This is maybe not the most technical explanation of it all, but this is how I understand it.