Reify symbol for type level String check at compile time

[sisoteuz]

Hello,

For the last couple of days I have tried to implement type level String check at compile time but it seems I cannot figure this out. Maybe what I try to achieve doesn’t make sense and I would love someone to clarify this for me.

Let’s say I have a data structure like so :

data Node (shape :: Symbol) = Node { id :: String, shape :: String }

Now I want to do operations on such nodes but only if they are of the same shape, so I have a function like the following which is trivial for simplicity sake :

doOnSameShape :: forall s. IsSymbol s => Node s -> Node s -> Effect Unit
doOnSameShape _ _ = let shape = reflectSymbol (SProxy :: SProxy s) in log $ "Shape is : " <> shape

All good so far, except I can lie to the compiler and “fake” the shape of a Node, for example this would compile fine :

doOnSameShape (Node { id : "x", shape : "circle" } :: Node "circle") (Node { id : "y", shape : "square" } :: Node "circle")

It compiles fine but we annotated the type of the second Node with “circle” whereas it is a “square”

And here is the problem, how can I make sure that Node are constructed with the right type depending on the shape field value ? I tried multiple things but none of them worked, my latest try is the following :

cons :: forall s. IsSymbol s => String -> String -> Node s
cons id shape = reifySymbol shape $ reifyNode (SProxy :: SProxy shape) id

reifyNode :: forall s1 s2. IsSymbol s1 => IsSymbol s2 => Compare s1 s2 EQ => SProxy s1 -> String -> SProxy s2 -> Node s1
reifyNode s id _ = Node { id : id, shape : reflectSymbol s }

With this I had hoped I could just do :

doOnSameShape (cons "x" "square") (cons "y" "square")

And the compiler would figure out the type of both cons calls, but I got very disappointed when the compiler threw the following error in the cons function at reifyNode call :

No type class instance found for
Prim.Symbol.Compare s2
                    sym3
                    EQ

I really don’t get what I need to do, if ever there is something to do to fix it at this point. Is it because of the signature of reifySymbol being :

reifySymbol :: String -> (forall sym. IsSymbol sym => SProxy sym -> r) -> r

Hence I will never be able to compare sym and my s Symbols ?

Many thanks in advance for your help

[sigilion]

Could you not write:

cons :: forall s. IsSymbol s => String -> SProxy s -> Node s
cons id shape = Node { id, shape: reflectSymbol shape }

[sigilion]

I think your typesignature is not correct, as it is equivalent to:

cons :: String -> String -> (forall s. IsSymbol s => Node s)

which is problematic, you want the s to be existentially not universally quantified.
To clarify something I don’t believe that reifySymbol is run at compile time, thus there is no way for the type checker to know that the two strings you enter are the same.

[hdgarrood]

I’m a little confused about your code. I don’t think this should compile:

cons :: forall s. IsSymbol s => String -> String -> Node s
cons id shape = reifySymbol shape $ reifyNode (SProxy :: SProxy shape) id

because there is no type variable shape in scope in the expression (SProxy :: SProxy shape).

Are you sure you want to keep track of the shape at both the type level and the value level? I suspect it would be easier if you used something like

newtype Node (shape :: Symbol) = Node { id :: String }

so that shape is a phantom type variable. You can then obtain a node’s shape as a string at runtime with

nodeShape :: forall shape. IsSymbol shape => Node shape -> String
nodeShape _ = reflectSymbol (SProxy :: SProxy shape)

[sigilion]

If you want to have compile time checked functions for shapes known at compile time, and be able to use those functions with shapes known only at runtime you could try:

data Node (shape :: Symbol) = Node { id :: String }

nodeShape :: forall shape. IsSymbol shape => Node shape -> String
nodeShape _ = reflectSymbol (SProxy :: SProxy shape)

nodeId :: forall s. Node s -> String
nodeId (Node {id}) = id

cons :: forall s. IsSymbol s => String -> SProxy s -> Node s
cons id shape = Node { id }

newtype ArbitraryNode = ArbitraryNode forall r. (forall s. IsSymbol s => Node s -> r) -> r

arbitraryShape :: ArbitraryNode -> String
arbitraryShape (ArbitraryNode x) = x nodeShape

arbitraryId :: ArbitraryNode -> String
arbitraryId (ArbitraryNode x) = x nodeId

arbitraryCons :: String -> String -> ArbitraryNode
arbitraryCons id shape =  ArbitraryNode \f -> reifySymbol shape \sym -> f (cons id sym)

forgetShape :: forall s. IsSymbol s => Node s -> ArbitraryNode
forgetShape x = ArbitraryNode \f -> f x

checkShape :: forall s. IsSymbol s => ArbitraryNode -> Maybe (Node s)
checkShape x = if arbitraryShape x == reflectSymbol (SProxy :: SProxy s) then Just $ Node {id: arbitraryId x} else Nothing

typify :: forall r sym. IsSymbol sym => SProxy sym -> (forall s. IsSymbol s => Node s -> Node s -> r) -> Node sym -> Node sym -> r
typify _ f = f

wrapFunction :: forall r. (forall s. IsSymbol s => Node s -> Node s -> r) -> ArbitraryNode -> ArbitraryNode -> Maybe r
wrapFunction f x y = reifySymbol (arbitraryShape x) \sym -> do
  x' <- checkShape x
  y' <- checkShape y
  pure $ typify sym f x' y'

[sisoteuz]

You are right my example didn’t compile, there was a typo in there, it should have been reifyNode (SProxy :: SProxy s). However I don’t strictly need to keep track of the shape at runtime so keeping the phantom type only is perfectly valid.

[sisoteuz]

Thank you so much for the very detailed example, I still need to get my around this as I’m fairly new to type level programming.

In your last example, I’m not too sure why I need ArbitraryNode, is it because I need to wrap a constructor of Node as the shape symbol is existentially quantified ?

Again thanks a lot for your example, I’m going to try it right now and figure out if it fits my use case.

[sigilion]

The ArbitraryNode is only if you want to be able to construct Nodes where the type is not known at compile time. You’re right, it is just a way of existentially quantifying the shape parameter.

[sisoteuz]

Just so that I get this straight (which I’m still figuring out). The purpose of typify is to “expose” the existentially quantified s from the function f at the upper level so that sym is specialized to that s. And this works because sym is universally quantified. Am I right ?

Also whenever we want to use functions with Node data type with shape values that are decided at runtime we need to carry a function that has an existentially quantified constraint IsSymbol then use ArbitraryNode as a back-and-forth converter between the compile world and the runtime world ?

[sigilion]

Just so that I get this straight (which I’m still figuring out). The purpose of typify is to “expose” the existentially quantified s from the function f at the upper level so that sym is specialized to that s. And this works because sym is universally quantified. Am I right ?

Not quite. The s in the function is the universally quantified one, typify specializes that to whichever type you want. The type we use is whichever one the existentially quantified sym has from the first ArbitraryNode.

Also whenever we want to use functions with Node data type with shape values that are decided at runtime we need to carry a function that has an existentially quantified constraint IsSymbol then use ArbitraryNode as a back-and-forth converter between the compile world and the runtime world ?

The ArbitraryNode effectively contains a fat pointer; it carries around a Node s, and a dictionary representing IsSymbol s for some type s that only it knows (this is the existential quantification). To use it you provide a function that takes one of these fat pointers (for any possible value of s), it specializes that function to its value of s and then calls the specialized function with its dictionary and node.

[sigilion]

This might be a slightly mode straightforward version of the last three functions (you don’t really need typify)

checkShape :: forall s. IsSymbol s => SProxy s -> ArbitraryNode -> Maybe (Node s)
checkShape shape x = if arbitraryShape x == reflectSymbol shape then Just $ Node {id: arbitraryId x} else Nothing

wrapFunction :: forall r. (forall s. IsSymbol s => Node s -> Node s -> r) -> ArbitraryNode -> ArbitraryNode -> Maybe r
wrapFunction f x y = reifySymbol (arbitraryShape x) \sym -> do
  x' <- checkShape sym x
  y' <- checkShape sym y
  pure $ f x' y'

[sisoteuz]

That makes much more sense now. Thank you for clarifying ! I think I start to get it now although I need to experiment more.

I tried to add a type level constraint to represent shapes that are different so that I can define another wrapFunction for that case. Here is the constraint:

class SameShape (s1 :: Symbol) (s2 :: Symbol) (res :: Boolean) | s1 s2 -> res
instance sameShape :: SameShape s s True
else instance notSameShape :: SameShape s s' False

Now let’s say I want to do something with nodes of different shapes:

onDifferentShapes :: forall s1 s2. IsSymbol s1 => IsSymbol s2 => SameShape s1 s2 False => Node s1 -> Node s2 -> String
onDifferentShapes _ _ = "shapes are different"

And my wrapper is like so:

wrapFunction :: forall r. (forall s1 s2. IsSymbol s1 => IsSymbol s2 => SameShape s1 s2 False => Node s1 -> Node s2 -> r) -> ArbitraryNode -> ArbitraryNode -> Maybe r
wrapFunction f x y = reifySymbol (arbitraryShape x) \sym -> do
    reifySymbol (arbitraryShape y) \sym' -> do
        x' <- checkShape sym x
        y' <- checkShape sym' y
        pure $ f x' y'

Finally the main :

main :: Effect Unit
main = do
    let x = arbitraryCons "foo" "square"
    let y = arbitraryCons "bar" "square"
    log $ show $ wrapFunction onDifferentShapes x y

The compiler complains on the call to f in wrapFunction saying that there is no type class instance found for SameRegion sym sym’ False.

I think I understand the problem which is that there is no such constraint defined for sym and sym’ of both reifySymbol and I can’t see a way to define such constraint.

Again I really appreciate the time you’ve spent helping me understand better type level programming.

[sigilion]

This is going to be a lot harder, as passing the same IsSymbol dict around and reifying/reflacting it was fairly straightforward, whereas convincing the compiler that it would have picked a specific typeclass instance for two unknown types is less so. I don’t know if purescript actually has the dependant type machinery necessary to do this “properly”, the only way I can think of doing this is to check the symbols are different and do an unsafeCoerse to eliminate the SameShape s s' False constraint, and I’m not sure I know enough about type class representations to do that safely.

[sisoteuz]

That makes sense as sym and sym’ are not known by compiler. I’ll stick with what I have so far based on your inputs and I think it’s good enough for what I want to achieve.

Wondering if we could achieve this kind of constraints in Haskell. Might give it a try later.