Haskell programlamada Monad ve kategori teorisinde Monad

Question

Haskell programlamasında kullanılan monad kavramı ve matematikte kategori teorisi hakkında bir sorum var.

Haskell'de bir monad aşağıdaki bileşenlerden oluşur:

• Her temel tür için karşılık gelen monad türünün nasıl elde edileceğini tanımlayan bir tür kurucusu. Bu tip kurucunun adı genellikle bütün monad ile eşanlamlı olarak kullanılır. Eğer$M$ monadın adı ve $t$ keyfi sabit veri türü ise $M t$ karşılık gelen monadik tip

• Temel tipin bir değerini karşılık gelen monad tipinin değeriyle eşleştiren bir birim işlevi. Sonuç, orijinal değerden elde edilebilen karşılık gelen türdeki "en basit" değerdir. Haskell'de bu işleve dönüş adı verilir. Birim işlevi polimorfik tiptedir$t → M t$

• Monadik işlemlerin kombinasyonunu tanımlayan en az bir başka işlem.

Öte yandan kategori teorisinde bir monad üçlüdür $(T, \eta, \mu)$ bir kategorinin $C$ nerede

• $T: C \to C$ bir functor

• $\eta: 1_K \to T$ kategori teorisi anlamında doğal bir dönüşüm

• $\mu: T^2 \to T$ doğal bir dönüşüm

ve bu nesneler aşağıdaki diyagramları sağlamalıdır: https://en.wikipedia.org/wiki/Monad_(category_theory)

Soru: Haskell'deki bu monadlar ile soyut kategori teorisi arasında nasıl bir ilişki var? Haskell'deki monad yapı, kategori teorisi anlamında doğal "monad yapıya" sahip mi, yani kanonik olarak$M$ yukarıda açıklandığı gibi bir kanonik üçlü?

Answer 1

Haskell'deki bir monadın, kategori teorisi tip teorisine dahili olarak yapıldığında, tip kategorisi üzerine bir monad olması amaçlanmıştır. Haskell ve benzer dillerin yetenekleri bir şekilde sınırlıdır, bu nedenle kategori teorisinde yapılamayacak birçok temel yapı vardır, ancak makul şekilde kodlanabilen birçok yapı vardır.

• M :: * → * onun yerine adlandırdığınız işlevin nesne eşlemesidir $T$ sonra.
• Functor'un ok eşleme kısmı şu şekilde verilir: fmap
• $η$Haskell'in çağırdığı birim işlevidir return(veya purebiraz daha genel olan)
• $μ$tarafından verilir join.

MonadÖrneklerden beklenen gereksinimler , kategori teorisinde monad olanlara eşdeğerdir.

Esasen, bu, özellikle kategorideki monadlar hakkında konuşmaktan çok da farklı değildir. $\mathsf{Set}$, Haskell / etc'den daha önce bahsedildiği gibi. teorinin sahip olduğu bazı yapıları kaçırmak ((ortak) ürünler gibi davranan, ancak geri çekilme / itme gibi olmayan şeyler vardır). Sadece monadları düşünerek çok şey yapabilirsin$\mathsf{Set}$, çünkü soyut / evrensel cebirdeki birçok yapı bir tane meydana getirir ve bu şekilde gösterilebilir.

Çeşitli programlama dillerindeki türlerin teknik olarak iyi özelliklere / yapıya sahip bir kategori oluşturmadığı tartışılabilir, ancak bunun yerine bunları System $F_ω$ve cevabı gerçekten ilginç bir şekilde değiştirmez.