Why is CatList Val and unsafeCoercion used instead of some type aligned sequence?

[safareli]

Today I finished reading of the referenced paper "Reflection without Remorse" (before I tried, but did not understood) and after that taking look at Free implementation made more sense but what I don't understand is why the CatList, Val and unsafeCoercion is used when some type aligned sequence could be used as in the paper?

[paf31]

Can you summarize the advantages? What is a "type aligned sequence" specifically? Can it be implemented as efficiently in PureScript?

[garyb]

The CatList usage is the type aligned sequence, is it not?

[safareli]

for example this is Type aligned binary tree (https://hackage.haskell.org/package/type-aligned-0.9.6)

data BinaryTree c x y where
  Empty :: BinaryTree c x x
  Leaf  :: c x y -> BinaryTree c x y
  Node  :: BinaryTree c x y -> BinaryTree c y z -> BinaryTree c x z

btw lists are Free Monoids and type aligned sequences are Free Categories and you can express make Free monoid From Free Categories if elements in this tree are of form:

type T a b c = T a

v :: T Number () ()
v = T 1

-- BinaryTree (T Number) () () is free monoid (list) of Number
z :: BinaryTree (T Number) () ()
z = Leaf v

CatList is not type safe i think and one needs to use the Val and unsafeCoercion. which could be avoided using BinaryTree like structure.

Advantage would be that it would not be depended on unsafeCoercion and would be typesafe. I don't think if it would significant impact on performance.

[safareli]

For example the Func type I wrote is basically type aligned binary tree whre data is on leafs specialised on (->) it could be generalised to type aligned binary tree for any binary type. and the Free I have is just TABinaryTree (->) and the ExpF is TABinaryTree (Kleisli Free)

[paf31]

What I meant was - can you write it without GADTs in an efficient way?

[safareli]

(it's fun that to fix quadratic complexity of Free monads bind you need to use Free category :d)

[safareli]

ah, don't know. GADT's have performance issues? after I read that paper and then looked at this implementation it raised this question nothing else, I have not even written purescript/haskell so don't know

[paf31]

Well we don't have GADTs 😄

[safareli]

ops didn't knew that.

is there plan/PR/issue on adding GADTs?

[paf31]

Doesn't look like it, but I'm sure it won't happen before 1.0, and probably not for a while after that.

[safareli]

what's the reason?

[garyb]

They're a huge feature for the typechecker, not something you can throw in there with a few days work.