5

FSharp Designer on downsides of Type Level Programming

 2 years ago
source link: https://lobste.rs/s/pkmzlu
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
FSharp Designer on downsides of Type Level Programming

Very insightful. I do find type level programming in Haskell (and, to a lesser extent, Rust) to be a confusing nightmare. Nonetheless, Rust could not exist without traits (i.e. without bounded polymorphism). The Sync and Send marker traits (combined with borrow checking) are the basis of thread safety.

I think Zig takes an interesting approach here, with it’s compile-time programming (i.e. type level programming with the same syntax and semantics as normal programming), but it suffers from the same typing issues as C++ templates, i.e. types are only checked after use and monomorphization. Rust’s bounded polymorphism can and is type checked before monomorphization, so you know if there are type errors in general. In Zig (and C++), you only know if there are type errors with a particular type, and only after using a function (template) on that type.

I think there’s room for an approach that’s more like Zig’s, but with sound polymorphic typing, using dependent type theory. Coq, Agda, and Idris include type classes (aka implicits, bounded polymorphism), but it doesn’t seem like type classes should be necessary in a dependently typed language. In particular, it doesn’t seem like they should provide any increase in expressiveness, though perhaps they reduce verbosity.

  1. Fwiw, even in Haskell you only really need one extension to obviate type classes in terms of “expressiveness,” namely RankNTypes. See https://www.haskellforall.com/2012/05/scrap-your-type-classes.html

    …though it doesn’t solve the verbosity issues. But I suspect that a language with better support for records might make this a pretty good solution (I have a side project where I am working on such a language).

    1. RankNTypes is my top pick for something to add to Haskell. however, for common cases type classes have the advantage of having decidable inference.

      1. Note that in the context of replacing type classes, the usual decidability problem with inference doesn’t really come up, because either way the higher rank types only show up in type definitions. E.g.

        class Functor f where
    fmap :: (a -> b) -> f a -> f b

        data Functor' f = Functor'
    { fmap' :: forall a b. (a -> b) -> f a -> f b
    }

        In the latter case, the problems with inference don’t come up, because the higher-rank quantifier is “hidden” behind the data constructor, so normal HM type inference can look at a call to fmap' and correctly infer that its argument needs to be a Functor' f, which it can treat opaquely, not worrying about the quantifier.

        You can often make typchecking advanced features like this easier by “cheating” and either hiding them behind a nominal type, or bundling them with a other features as a special case.

        (N.B. I should say that for just Functor' you only need Rank2Types, which actually is decidable anyway – but I don’t think GHC actually decides it in practice, so it’s kindof a nitpick).

        Of course this is talking about type inference, whereas type classes are really more about inferring the values, which, as I said, this doesn’t solve the verbosity issues.

  2. Type classes aren’t just about verbosity, global coherence is a very important aspect. Any decision on whether to use a type class vs. explicit dictionary passing needs to consider the implications of global coherence. I think Type Classes vs. the World is a must-watch in order to engage in productive discussion about type classes.


report

Recommend

About Joyk


Aggregate valuable and interesting links.
Joyk means Joy of geeK