Andy Melnikov (nponeccop) wrote,
Andy Melnikov
nponeccop

Categories:

О fixed point

http://conal.net/blog/posts/semantic-editor-combinators

newtype (g :. f) a = O { unO :: g (f a) }

inO :: (g (f a) -> g' (f' a')) -> ((g :. f) a -> (g' :. f') a')
inO h (O gfa) = O (h gfa)

instance (Functor g, Functor f) => Functor (g :. f) where
  fmap  = inO.fmap.fmap
 
instance (Applicative g, Applicative f) => Applicative (g :. f) where
  pure  = O . pure . pure
  (<*>) = (inO2.liftA2) (<*>)
Исходя из плотности мысли и определений, выглядящих как self-referential, данную работу надо запретить как развращающую неокрепшие умы.

Но у меня два вопроса:

1) Есть ли какая-то теорема, в духе того, что все конечные fixed points в денотационной семантике являются функциями?

Я сам не местный и денсем не знаю. На пальцах, скажем, x = 1 : x ничем c виду не отличается от f = \x -> if x == 0 then 1 else f (n - 1) * f, но x нефункция и бесконечен, а f - функция и конечна. Всегда ли так или есть исключения?

2) Есть ли какие-либо способы решать уравнения этих двух видов, сильно непохожие на то, что сделано в Хаскеле? Речь в этом вопросе идет конечно, о реализации языка программирования, а не о денотационной семантике.
Tags: fp, programming
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 20 comments