Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

Atrium > Mathematics, Physics & Philosophy: (infinity)-Haskell

Bottom of Page

1 to 11 of 11

  1.  
    • CommentRowNumber1.
    • CommentAuthorMirco Richter
    • CommentTimeJun 30th 2012
    • (edited Jun 30th 2012)
    Does anyone know, if there are any attempts to extend the Haskell programming language, from its 'ordinary category style' into the direction of the nPoint of view?

    Anyone ever used Haskell for some time knows that the way it works is greatly influenced by category theory thinking. Functors, monads ect. all are natural concepts there. Recently this made me thinking if there is research going on towards homotopy types or lets just say nPoint-thinking in Haskell?

    (Don't want to rule out other languages, but I'm under the impression that this on is best suited here)

    Hmm... But on a first thought even the representation of a true (not truncated) infinity category in physical memory is not obvious....

  2. You probably know that there is a haskellwiki which I linked from Haskell. You could ask the community there, too.

    • CommentRowNumber3.
    • CommentAuthorMirco Richter
    • CommentTimeJun 30th 2012
    I know, but I had the hope that experts from Homotopy Type Theory are a better address for a first try... Maybe Mike knows something?
    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeJun 30th 2012
    • (edited Jun 30th 2012)

    Mike seems to be busy.

    As far as I am aware, aspects of HoTT have been implemented only in Coq and, more recently, in Agda: this was announced here.

    I have never heard any HoTT person mention an implementation in Haskell.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeJun 30th 2012

    Yes, Mike is busy right now and only checking the nPlaces every few days. (-:

    Among non-dependently-typed programming languages, functional ones such as Haskell and ML are certainly the most closely related to category theory. But I don’t know of much of any way to do higher category theory without dependent types. I would regard Agda (used from a HoTT PoV) as precisely an “extension” of Haskell to the nPOV; the syntax of Agda is very similar to Haskell and I believe Agda is actually written in Haskell. Coq is similarly related to ML.

    • CommentRowNumber6.
    • CommentAuthorMirco Richter
    • CommentTimeJun 30th 2012
    Ok. So I'll have a look at Agda. Sounds promising ...
    • CommentRowNumber7.
    • CommentAuthorNikolajK
    • CommentTimeApr 11th 2016

    I’ve extended on my text on what’s supposed to be a back and forth translation for people that know Haskell concepts and people that know category theory from their math education. I might do more of that in the future, and maybe for other languages too.

  8. Cool, thanks! We should also record the use of free monads (the free monad functor is left adjoint to the forgetful functor from monads to endofunctors), the recent “freer monads” (the “freer monad” functor is left adjoint to the forgetful functor from monads to endomaps of the set of objects), and Kan extensions in Haskell. I’ll contribute a bit in this direction when I have time.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeApr 11th 2016

    Regarding connections with HoTT, higher inductive types are naturally explained using “presented” monads (a generalization of free ones). There are some slides about this on my web site (sorry for being terse now, my laptop died and I’m reduced to a tablet at home for a while).

    • CommentRowNumber10.
    • CommentAuthorNikolajK
    • CommentTimeApr 12th 2016

    @Mike: Since I saw you editing that section in the Wikipedia HoTT article,

    with the type equivalence definition via f∘g=idf \circ g = id and h∘f=idh\circ f=id, it speaks of “suitably choosen” gg and hh for the to-be equivalence ff. Does it have a Special name if gg and gg coincide?

    What I also like to understand, in a type system in which univalence is implemented, can I set up a category as a type or class (one of groups, say, potentially a higher category) and make the group isomorphisms become the equivalences (so I can always also turn them into equalities)?

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeApr 12th 2016

    The Wikipedia article is pretty terrible, don’t try to learn HoTT from it. I only occasionally try to fix the most egregious errors. Your questions are both answered in the HoTT book: if g=h we call it a quasi-inverse, or a half-adjoint equivalence if there is an extra coherence datum given; and naturally-ocurring categories have that property already, while any category can be universally ’saturated’ to have it.

1 to 11 of 11

  1.