Splitting type-level strings by period

Hey all, I’m working on a binding/DSL combo for GoJS. I’m trying to create an easy way to handle nested foreign data types. I want to be able to do get @"field1.nestedField" someOpaqueType without having to write all possible combinations of symbols, for obvious reasons. Here’s what I have:


class Split (withPeriod :: Symbol) (prePeriod :: Symbol) (postPeriod :: Symbol) | withPeriod -> prePeriod postPeriod, prePeriod postPeriod -> withPeriod
instance (
  Cons "." postPeriod periodAndPost,             -- split periodAndPost only in "." and the rest
  Cons postPeriodHead postPeriodTail postPeriod, -- split the rest
  Equals postPeriodHead "." False,               -- assert that the head of the rest is NOT "."
  Cons prePeriodHead prePeriodTail prePeriod,    -- split prePeriod
  Equals prePeriodHead "." False,                -- assert that the head of prePeriod is NOT "."
  Append prePeriod periodAndPost total           -- join prePeriod and periodAndPost
  )          
  => Split total prePeriod postPeriod

class Get (prop :: Symbol) (d :: Type) (t :: Type) | d prop -> t

instance Get "part" GraphObject_ Part_
else instance Get "subject" DiagramEvent_ a
else instance Get "diagram" DiagramEvent_ Diagram_
else instance Get "isModified" Diagram_ Boolean
else instance Get "isReadOnly" Diagram_ Boolean
else instance getNested :: (Split total prePeriod postPeriod, Get prePeriod d fieldType, Get postPeriod fieldType nestedType) => Get total d nestedType

foreign import get_ :: forall d a. d -> String -> a 

get :: forall @s @d b. IsSymbol s => Get s d b => d -> b
get d = get_ d (reflectSymbol (Proxy @s))

-- This works:
someFn :: DiagramEvent_ -> Boolean
someFn e = let
  d :: Diagram_
  d = get @"diagram" e
  in
   get @"isModified" d

But this:

someFn2 :: DiagramEvent_ -> Boolean
someFn2 = get @"diagram.isModified"

doesn’t compile with this error:

No type class instance was found for

    Prim.Symbol.Cons "."
                     t1
                     t2

  The instance head contains unknown type variables. Consider adding a type annotation.

while solving type class constraint

  GoJS.FFI.Split "diagram.isModified"
                 t0
                 t1

while checking that type forall (@d :: Type) (b :: Type). IsSymbol "diagram.isModified" => Get "diagram.isModified" d b => d -> b
  is at least as general as type DiagramEvent_ -> Boolean

The constraint GoJS.FFI.Split "diagram.isModified" t0 t1 should be determining t0 and t1 to be "diagram" and "isModified", as per the functional dependency in the class Split, so it should know, by matching periodAndPost with ".isModified", that t1 is its tail of it.

I’m pretty puzzled because the Split class seems to be correct; if I use the repl to try and print a reflected symbol like:

myVal :: Split "where.ami" w a => String
myVal = reflectSymbol (Proxy @w)

it works. What am I doing wrong?

Might be related to this bug? Functional dependencies do not propagate to subclasses · Issue #2397 · purescript/purescript · GitHub

@amuricys I suggest to write a type level test for the Split class. It could look like this:

testSplit :: forall @sym @before @after. Split sym before after => Unit
testSplit = unit

Now we can write some tests:

This compiles, so it looks like that it’s correct if all variables are given.

testSplit1 :: Unit
testSplit1 = testSplit @"foo.bar" @"foo" @"bar"

You can also verify that it does not work for wrong inputs. This does not compile:

--X testSplit1 :: Unit
--X testSplit1 = testSplit @"foo.bar" @"bar" @"foo"

But do the functional dependencies work as well? Does it work if only some type variables are given?

It turns out that the first functional dependency is not working:

--X testSplit2 :: Unit
--X testSplit2 = testSplit @"foo.bar" @_ @_

Likewise the second one:

--X testSplit3 :: Unit
--X testSplit3 = testSplit @_ @"foo" @"bar"

Hope that’s helpful o narrow the problem, I think you need to fix the Split class first to make those tests pass.

2 Likes

Thank you for the suggestion! I tried to rethink this by using recursion (it’ll be necessary to handle an arbitrary number of period separated names after all), and I got stuck. I reduced the problem to even the most basic type-level string operation, to realize that I don’t understand how the compiler recurses on instances at all. This already breaks:

class DropUntilPeriod (inp :: Symbol) (post :: Symbol) | inp -> post
instance baseCase :: (
    Cons "." post inp
    ) => DropUntilPeriod inp post
else instance recursiveCase :: (
    Cons h tail inp,
    DropUntilPeriod tail post
) => DropUntilPeriod inp post

myTest :: forall @toSplit post. IsSymbol post => DropUntilPeriod toSplit post => String
myTest = reflectSymbol (Proxy @post)

myTestStr :: String
myTestStr =  myTest @"ab.def"

The error is:

Could not match type

    "a"

  with type

    "."


while solving type class constraint

  Prim.Symbol.Cons "."
                   t0
                   "ab.def"

It looks to me like the compiler tries the first instance and IMMEDIATELY gives up. Even if I change the second instance in the chain to be trivial like so:

class DropUntilPeriod (inp :: Symbol) (post :: Symbol) | inp -> post
instance baseCase :: (
    Cons "." post inp
    ) => DropUntilPeriod inp post

-- Should match absolutely anything
else instance DropUntilPeriod a a

I still get the same error. It’s almost embarrassing to be stuck on something so (seemingly) trivial at the type level.

Yes, the compiler commits to an instance based on the instance head: ... => DropUntilPeriod inp post matches everything, so the first one will always chosen. as a second step it will be checked if the constraints hold. But if not, it will not skip to the next instance. Even if it’s an instance chain (using “else”).
So what you need it a way to pattern match in the instance head:

instance (...) => DropUntilPeriod "." post
else instance (...) => DropUntilPeriod other post

I experimented with this kind of type level parsers lately. And for me it worked best to always carry around a head and a tail of the symbol. (Unfortunately there’s no typelevel Char). Anyways, you have to take care of the empty symbol as base case in the recursion. I did this by introducing another type class wrapping the one that pattern matches. You can see the see the pattern applied in this file.

1 Like

AH!!! That’s what I was missing. Thanks Michael, this works:

class DropUntilPeriod (h :: Symbol) (t :: Symbol) (post :: Symbol) | h t -> post
instance baseCase :: DropUntilPeriod "." t t
else instance 
    (
        Cons h t tail,
        DropUntilPeriod h t out
    ) =>
    DropUntilPeriod head tail out

class DropUntilPeriodWrap (inp :: Symbol) (post :: Symbol) | inp -> post
instance 
    (
        Cons h t inp,
        DropUntilPeriod h t post
    ) =>
    DropUntilPeriodWrap inp post 

myTest :: forall @inp @post. IsSymbol post => DropUntilPeriodWrap inp post => String
myTest = reflectSymbol (Proxy @post)

myTestStr :: String
myTestStr =  myTest @"bc.def" @_ -- results in "def"

A bit strangely, using Append instead of Cons doesn’t on the head of the string. I’d think they’d be equivalent on a single-char symbol h, but I think Cons has extra built-in properties.

For completeness, here’s the original class I was trying to implement (only works if a string has a . in it, but that’s fine):

class SplitOnPeriod (h :: Symbol) (t :: Symbol) (acc :: Symbol) (pre :: Symbol) (post :: Symbol) | h t -> pre post
instance baseCase :: SplitOnPeriod "." t acc acc t
else instance 
    (
        Cons h t tail,
        Append acc head accPlus,
        SplitOnPeriod h t accPlus pre post
    ) =>
    SplitOnPeriod head tail acc pre post

class SplitOnPeriodWrap (inp :: Symbol) (pre :: Symbol) (post :: Symbol) | inp -> pre post
instance 
    (
        Cons h t inp,
        SplitOnPeriod h t "" pre post
    ) =>
    SplitOnPeriodWrap inp pre post

myTest :: forall @inp pre post. IsSymbol post => IsSymbol pre => SplitOnPeriodWrap inp pre post => String
myTest = reflectSymbol (Proxy @pre) <> " , " <> reflectSymbol (Proxy @post)

myTestStr :: String
myTestStr =  myTest @"bc.def"

Thanks again :slight_smile:

1 Like