Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How does Frege generalize number literals?

Tags:

haskell

frege

It appears that Frege can evaluate

1/2

to return the Double value 0.5.

The literal 1 is of type Int. It seems to be promoted to Double, which is a type in the Real class and thus knows the / operator. How does this happen? Is it using the Haskell approach of silently replacing the literal 1 with fromInt 1 or is something else going on? How is Double chosen as the instance of Real to use here? Is there a list of "default" instance types like in Haskell?

like image 961
Dierk Avatar asked Jun 16 '15 10:06

Dierk


1 Answers

Simple decimal literals without type indicator (i.e. one of the letters lndf) do not automatically have type Int in Frege.

They will get assigned the type you probably wanted, and the literal will get adapted accordingly. This is why they are called DWIM (do what I mean) literals.

This is mentioned in the "Differences to Haskell" document. And it should be also in the language reference manual, of course. If it isn't there yet, it must be because the author is extremely lazy.

In brief, DWIM works like this: when the type checker sees the literal the first time, it just assigns a type variable for it, plus a Num constraint for that type variable. Later, in a second pass, it finds all DWIM literals. And now, the type variable is in one of the following states :

  1. unified with some type, like Long, Double or the like. The literal will be typed accordingly.
  2. Unified with some other type: this is an error.
  3. Unified with a type variable from a type signature: the literal gets replaced with an application of fromInt to the literal typed as Int.
  4. Not unified at all: if the type variable is constrained by (a subtype of) Real the type is Double otherwise Int.

In your example, the literals are typed Double because of the Real constraint of the division operator.

A similar approach is taken for literals with decimal point, however, they start out with a Real constraint, and can thus end up as Float or Double or application of fromDouble.

Note that except for case 3 there is no type conversion or type cast at runtime.

The reason literals are not generally overloaded like in Haskell is to avoid unnecessary class constraints, because their implementation tends to result in expensive code. Also, since we don't have monomorphism restriction, you could have polymorphic constants accidentally. (Think fibs = 1:1:...)

With DWIM literals, you get monomorphic constants and functions unless you require otherwise with a type annotation.

like image 102
Ingo Avatar answered Sep 22 '22 01:09

Ingo