1. 30
  1. 4

    I don’t know much Haskell, so I don’t understand what Left, Right and M.Map do. But is attempt 2 basically isomorphic to Rich Hickey’s criticism of Haskell that it can’t unify T with Maybe T?

    1. 7

      Left and Right are data constructors for the Either a b type. This is a basic sum type, it’s holds either an a or a b, but not both. Pattern matching on an Either a b you see whether it’s a Left x or a Right x and then you know either x : a or x : b.

      M.Map is a type constructor of type K -> V -> M.Map K V, where M.Map K V is a key-value map with keys of type K and values of type V.

      But is attempt 2 basically isomorphic to Rich Hickey’s criticism of Haskell that it can’t unify T with Maybe T?

      This totally misses the point of Haskell. You can’t ‘unify’ two values of different types. A function of type Maybe T -> T has an error on the None branch allowing it to type check.

      T -> Maybe T is the type of Just. Obviously Haskell has that.

      1. 3

        I’m not a fan of Rich Hickey or his views about type systems, but let’s do a little more justice to his argument about Maybe T; He says that if I’m calling a function that expects a Maybe T, but if I’m calling it with a T, why can’t the compiler be smart enough to adapt the T by inserting a Just in front of it. So, in effect, he wants T to be a subtype of Maybe T and he wants Haskell’s type system to have contravariance w.r.t. subtyping.

        Even though what he wants seems reasonable to a first approximation, he doesn’t mention what should happen if the type is Maybe a for a polymorphic a, and if I try to pass in Maybe Int. Should it become Maybe (Maybe Int) or just Maybe Int? In my view, the road to programmer hell is paved with naive intentions of taking petty shortcuts like this.

    2. 3

      This does seem like an ideal use case for depedent types. Here’s one solution in Idris (note I’m using Int instead of Rational for convenience):

      module Main
      data Currency
        = USD
        | EUR
      implementation Show Currency where
        show USD = "USD"
        show EUR = "EUR"
      data Money : Currency -> Type -> Type where
        MkMoney : (c : Currency) -> Int -> Money c Int
      implementation Show (Money c Int) where
        show (MkMoney c i) = (show i) ++ " " ++ (show c)
      plus : Money c Int -> Money c Int -> Money c Int
      plus (MkMoney _ x) (MkMoney _ y) = MkMoney _ (x + y)
      main : IO ()
      main = do
        putStrLn $ show $ plus (MkMoney USD 1) (MkMoney USD 2)
        -- this won't compile
        -- putStrLn $ show $ plus (MkMoney USD 1) (MkMoney EUR 2)
      1. 3

        One thing I always wonder with the dependent types is what happens when you find out you want to move something from compile time to runtime. E.g., suppose requirements changed and your program now has to run with a configuration file that lists allowable currencies. Could you bring those values to the type level, or would that change mean rewriting all the types?

        1. 3

          I’m still quite new to dependent types (an enthusiastic learner!) but my understanding here is that with untrusted input, you need to convince the compiler that it is an instance of a particular data type (similar to parsing in Haskell or other MLs). Once you do so, you get the same power described above.

          This does assume that you have the correct representation of the types inside the code as well. I’m not sure if there’s the ability to generate types from some outside configuration, though I do know that any type-level code in Idris must be total and pure. I’m guessing that things like “reading from the filesystem while compiling your program” are a no-no.

          1. 3

            Idris does indeed have type providers, which give you IO actions evaluated at compile-time to give a constant value available at run-time, and (of course) the return value can even be a type!

            1. 1

              Fascinating, thanks for sharing this.

      2. 3

        I’ve played a little in this space but not with production code. Interesting to see your exploration. Some remarks, in no particular order:

        • Getting the primitives like plus and mult seemed easy, so have you tried putting your unsafePlus/plus-style split at a higher level, where maintaining type-safety starts getting hard?

        • safe-money, which you looked at in section 3, also provides a couple of types whose names start with Some, like SomeDiscrete. These hold an amount of “some” currency, and you can “downcast” using fromSomeDiscrete :: (KnownSymbol currency, GoodScale scale) => SomeDiscrete -> Maybe (Discrete' currency scale).

        • There is a typo, in footnote 2: “GBP is a Great British Pound (£). USD is United States Dollars (£), and JPY is Japanese Yen (¥)” - Wrong currency sign for USD.

        1. 2

          As I pointed out in reddit, this seems like an appropriate use case for the dependent-map library.

          1. 1

            There are simpler ways, though that one isn’t bad if you hide it behind a nicer API.