Tony Morris

@EyalL @kaleidic Yes, it implements a bunch of ceremonious nonsense. Is that OO to you?

@dibblego @kaleidic it implements a form of oo, yes

@EyalL @kaleidic a "form of OO"? I didn't even know there were forms. Is that like sectarianism? More and more questions fall out.

@dibblego @kaleidic Haskell and Agda are different "forms of fp"

@EyalL @kaleidic Since I am an optimist, I am going to pretend that was a joke I did not understand, instead of a false statement.

@dibblego why false? Haskell has semi dependent fp with vals/kinds/sorts. Agda has full dependent types without hard coded "levels"

@EyalL Everything you just said is true, and completely unrelated to the functional programming thesis.

@dibblego then we're arguing terminology. FP:Agda/Haskell ~~ oo:OOHaskell/Smalltalk.