How to convert List to Record at the type level?

Help
, , ,
#1

I’m writing a complex type-level arithmetic, here’s a simplified example.

I wrote some types first:

data MyList :: Symbol -> Type -> Type
data MyList a b
  = My_Cons (Proxy a) b

data MyList_Nil :: Type
data MyList_Nil
  = My_Nil

Then write some functions that operate on it:

mkList :: MyList_Nil
mkList = My_Nil

class AddItem list where
  addItem :: forall newVal. (Proxy newVal) -> list -> MyList newVal list

instance AddItem MyList_Nil where
  addItem newVal list = My_Cons newVal list

instance AddItem (MyList a tail) where
  addItem newVal list = My_Cons newVal list

class ShowList list where
  showList :: list -> String

instance ShowList MyList_Nil where
  showList _ = "Nil"

instance (IsSymbol a, ShowList tail) => ShowList (MyList a tail) where
  showList (My_Cons a tail) = reflectSymbol a <> "," <> showList tail

Just use them like this:

  log $ showList $ mkList -- "Nil"
  log $ showList $ addItem (Proxy :: Proxy "x1") $ mkList -- "x1,Nil"
  log $ showList $ addItem (Proxy :: Proxy "x2") $ addItem (Proxy :: Proxy "x1") $ mkList -- "x2,x1,Nil"

Now, I want to convert them to Record.
E.g:
MyList_Nil → {}
MyList "x" MyList_Nil → {x :: String}
MyList "x1" (MyList "x2" MyList_Nil) → {x1 :: String, x2 :: String}

I try this, but it doesn’t work:

class ListToRow :: forall k1. Type -> k1 -> Constraint
class ListToRow list r | list -> r

instance ListToRow MyList_Nil ()
instance ListToRow (MyList a MyList_Nil) (a :: String)
instance (ListToRow tail s1, Union (a1 :: String) (a2 :: String) s2, Union s1 s2 s) => ListToRow (MyList a1 (MyList a2 tail)) s

foreign import f :: forall a tail s. ListToRow (MyList a tail) s => (MyList a tail) -> Record s

-- expect the type of x to be: {x1 :: String}
-- The actual type is: {a :: String}
x = f $ addItem (Proxy :: Proxy "x1") $ mkList

I thought about using RowList, but that doesn’t work either, because RowList can’t infer Row.

class ListToRowList :: forall k1. Type -> k1 -> Constraint
class ListToRowList list r | list -> r

instance ListToRowList MyList_Nil ()
instance ListToRowList (MyList a MyList_Nil) (RL.Cons a String RL.Nil)
instance (ListToRowList tail s1, Union (a1 :: String) (a2 :: String) s2, Union s1 s2 s, RowToList s rl) => ListToRowList (MyList a1 (MyList a2 tail)) rl

foreign import f :: forall a tail r rl. RowToList r rl => ListToRowList (MyList a tail) rl => (MyList a tail) -> Record r

-- expect the type of x to be: {x1 :: String}
-- The actual type is: forall t148. RowToList t148 (Cons "x1" String Nil) => Record t148
x = f $ addItem (Proxy :: Proxy "x1") $ mkList

this is all the code

Are there other methods, like RowListToRow? or RowListToRecord?
Please tell me more tips on type-level manipulation.
Thx

#2

I made it!

I used this library

this is my code

Need to add this in ‘packages.dhall’ file:

let upstream =
      https://github.com/purescript/package-sets/releases/download/psc-0.14.7-20220404/packages.dhall
        sha256:75d0f0719f32456e6bdc3efd41cfc64785655d2b751e3d080bd849033ed053f2

in  upstream
  with typelevel-eval =
      { dependencies =
        [ "bifunctors"
        , "contravariant"
        , "control"
        , "effect"
        , "either"
        , "leibniz"
        , "prelude"
        , "profunctor"
        , "psci-support"
        , "tuples"
        , "typelevel-prelude"
        , "unsafe-coerce"
        ]
      , repo =
          "https://github.com/natefaubion/purescript-typelevel-eval.git"
      , version =
          "v0.5.0"
      }
#3

You could also write ListToRow like this.

class ListToRow :: forall k. Type -> Row k -> Constraint
class ListToRow l r | l -> r

instance ListToRow MyList_Nil ()
else instance (ListToRow xs q, Row.Cons x String q r) => ListToRow (MyList x xs) r

listToRecord :: forall l r. ListToRow l r => l -> Record r
listToRecord = unsafeCoerce

x0 :: {}
x0 = listToRecord mkList

x1 :: { x1 :: String }
x1 = listToRecord $ addItem (Proxy :: _ "x1") mkList

x2 :: { x1 :: String, x2 :: String }
x2 = listToRecord $ addItem (Proxy :: _ "x2") $ addItem (Proxy :: _ "x1") mkList

Note that this is all type-level and the listToRecord function isn’t properly implemented, although one way to approach implementing that would be to add a method in ListToRow that takes advantage of the recursive instances.

Oh, and for v0.15.x, constraints in foreign import declarations like this are disallowed:

foreign import f :: forall a tail s. ListToRow (MyList a tail) s => (MyList a tail) -> Record s
2 Likes
#4

Wow, so cool!
I hadn’t thought of using Row.Cons to parse labels of row.
Thanks answer, I get it!

1 Like