What's the reason "tagless final" is called that? Is it because the actions don't have "tags" (i.e. supposedly no runtime repr.), and instead are just instantiated at one point in the end before being run ("final", via transformers)?
As far as "final" goes, I remember something about it being slightly arbitrary name for "function-based representation / Church-like encoding" in comparison to "initial" encoding which uses normal data constructors
MonadSomething m => m a is in a sense final encoding of program represented as function taking MonadSomething dictionary and calling it's methods as constructors of actions inside of the program
Compare it to Free Something a, where Something is some Functor with the actions as normal constructors
We can do a similar trick to the Church encoding of lists and represent our data constructors as functions. This is not a Church encoding; it's called a final encoding for reasons unknown to me. The version using explicit constructors is called an initial encoding.
I found an answer by one of the authors of the original paper:
The 'final' in 'finally tagless, partially evaluated' (the original paper that you skipped over) is an adjective qualifying 'tagless', and is a pun on partial evaluation's tagging-untagging problem. It does allude to final semantics (since 'final tagless' is really specifying an algebra via its polymorphic fold in a way that prevents 'peeking', unlike all initial algebra based methods) because all you can do is to call the fold. But it's still not 'final' in any reasonable way, even though there's dualities galore lurking around the corner.
The Haskell and Scala community have been very enamored recently with what they call tagless final 'pattern' of programming. These are referenced as dual to initial free algebras, so I was wonderin...
What's the reason "tagless final" is called that? Is it because the actions don't have "tags" (i.e. supposedly no runtime repr.), and instead are just instantiated at one point in the end before being run ("final", via transformers)?
(which seems to not currently be true for
mtl)As far as "final" goes, I remember something about it being slightly arbitrary name for "function-based representation / Church-like encoding" in comparison to "initial" encoding which uses normal data constructors
how is mtl related to Church encoding?
(also, I know the term is more popular in scala, maybe it means something different there? :thinking: )
MonadSomething m => m ais in a sense final encoding of program represented as function takingMonadSomethingdictionary and calling it's methods as constructors of actions inside of the programCompare it to
Free Something a, whereSomethingis someFunctorwith the actions as normal constructorsHmm, or maybe Scott encoding would be a better fit
https://peddie.github.io/encodings/encodings-text.html
this looks like it explores this question specifically
even features a quote by @Ben Kolera !
so it's like Church, but different
It's best to read the original sources to find answers like this: "Finally Tagless, Partially Evaluated".
http://okmij.org/ftp/tagless-final/#tagless-final
I found an answer by one of the authors of the original paper:
https://cstheory.stackexchange.com/questions/45565/what-category-are-tagless-final-algebras-final-in#comment101261_45565
what other "initial algebra methods" are there?
besides
FreeI think that's "the definition" of an initial algebra thingy
so, none?
but Steven's quote says "all initial algebra based methods"
like, when you're defining a datatype formally (which is what adts in hs are), you're defining it as something generated as a fixpoint (so Free)
ADTs in hs are formally defined datatypes?
what does that mean
FDDTs
I meant to say that if you want to formalise what an "adt" (in the hs sense) means in mathematics, you would (traditionally) do so via fixpoints
(as you also do with recursive functions)
ah
@Georgi Lyubenov // googleson78 did you maybe mean
Fixhere?yup! thanks