Prioritize readability with Pos1, Pos2, ... constructors? #5

Closed
bjornbm opened this Issue Mar 2, 2014 · 3 comments

Comments

Projects
None yet
2 participants
Owner

bjornbm commented Mar 2, 2014

I'm considering rewriting again with

data NumType = Neg10Minus Nat
             | Neg9
             ...
             | Neg1
             | Zero
             | Pos1
             | Pos2
             ...
             | Pos9
             | Pos10Plus Nat

Advantage: error messages will always say Pos4 rather than Pos1Plus (S (S (S Z))) which I feel will be advantageous when debugging code using dimensional. I'm also hoping that it will almost always be possible to get the “original” numtypes in error messages, e.g. "Could not match Pos4 with Pos2”, rather than the reduced ones (“Could not match Pos1Plus (S Z) with Zero”).

Disadvantage: updating all the type families in NumType.dk will be cumbersome, but trivial.

Owner

bjornbm commented Mar 5, 2014

Take a look at https://github.com/bjornbm/numtype-dk/blob/readable/Numeric/NumType/DK.hs

While it is very verbose, it will actually give you decent error messages when the types don't match up (at least for NumTypes < 10 which should be sufficient for realistic uses of dimensional). E.g.:

*Numeric.NumType.DK> toNum $ pos9 / neg4

<interactive>:3:1:
    Could not deduce (KnownNumType ('Pos9 / 'Neg4))
      arising from a use of ‛toNum’
    from the context (Num s)
      bound by the inferred type of it :: Num s => s
      at <interactive>:3:1-19
    In the expression: toNum
    In the expression: toNum $ pos9 / neg4
    In an equation for ‛it’: it = toNum $ pos9 / neg4

Versus master:

*Numeric.NumType.DK> toNum $ pos9 / neg4

<interactive>:9:1:
    Could not deduce (KnownNumType
                        (Negate (((t0 + Pos1) + Pos1) + Pos1)))
      arising from a use of ‛toNum’
    from the context (Num s)
      bound by the inferred type of it :: Num s => s
      at <interactive>:9:1-19
    The type variable ‛t0’ is ambiguous
    Note: there are several potential instances:
      instance KnownNumType ('Pos1Plus n) => KnownNumType ('Neg1Minus n)
        -- Defined at Numeric/NumType/DK.hs:202:10
      instance KnownNumType (Pred ('Pos1Plus n)) =>
               KnownNumType ('Pos1Plus n)
        -- Defined at Numeric/NumType/DK.hs:199:10
      instance KnownNumType 'Zero
        -- Defined at Numeric/NumType/DK.hs:197:10
    In the expression: toNum
    In the expression: toNum $ pos9 / neg4
    In an equation for ‛it’: it = toNum $ pos9 / neg4

<interactive>:9:9:
    Occurs check: cannot construct the infinite type:
      t0 ~ Negate (Negate (t0 + Pos1) + Pos1)
    The type variable ‛t0’ is ambiguous
    Expected type: Proxy (Negate (((t0 + Pos1) + Pos1) + Pos1))
      Actual type: Proxy (Pos9 / Neg4)
    In the second argument of ‛($)’, namely ‛pos9 / neg4’
    In the expression: toNum $ pos9 / neg4
    In an equation for ‛it’: it = toNum $ pos9 / neg4

(Of course, in general the “In the expression” part of the error message will not be as helpful as in this example.)

Collaborator

dmcclean commented Mar 5, 2014

Works for me.

Owner

bjornbm commented Mar 5, 2014

Closed with 2326579.

@bjornbm bjornbm closed this Mar 5, 2014

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment