Overview

LambdaCube 3D is specified as Haskell98 plus various language extensions.

Haskell98 language features

• patterns
  • variable, constructor, wildcard – Done
  • tuple, list – Done
  • at-pattern – Done
  • irrefutable pattern – TODO
• expressions
  • variable, constructor, application, lambda, case, if – Done
  • let – WIP
  • type signature – Done
  • tuples, lists – Done
  • list comprehensions – Done
  • dot-dot expressions – WIP
  • do syntax – TODO
  • operators, fixity declarations – Done
• definitions
  • value definition, function, function alternative, guard, where-block – Done
  • mutual recursion – TODO
  • type signature – WIP
  • data declarations – Done
  • newtype declarations – TODO
  • type synonyms – TODO
  • type classes – WIP
    • defaulting – TODO
    • deriving – TODO
• modules
  • module imports and export lists – WIP

There are some diversions from Haskell98. Our plan is to keep this list very short.

• Different Prelude – WIP
• Definitions should be ordered bottom-up – *

Extentions compared to Haskell98

These extensions are automatically enabled.

Registered extensions

• NoMonomorphismRestriction – Done
• NoNPlusKPatterns – Done
• TypeApplication – Done
• KindSignatures – Done
• EmptyDataDecls – TODO
• PolyKinds & DataKinds – WIP
• GADTs (includes ExistentialQuantification) – WIP
• TypeFamilies – WIP
• PartialTypeSignatures – WIP
• ScopedTypeVariables – TODO
• RankNTypes – TODO
• Typed holes – TODO
• LambdaCase – TODO
• LANGUAGE pragmas
  • NoImplicitPrelude – Done

Other extensions

• Row polymorphism – Done
• Swizzling – WIP
• Compositional typing – Done
• ImplicitParams – WIP
• Type error specialisation – TODO

Prelude

The current Prelude

Row polymorphism

A.k.a. structural records.
Row polymorphism is implemented following Edward Kmett’s presentation on Ermine.

v1 = {x: 1.0, y: 2.0, z: 3.0}
v2 = {x: 1.0, y: 2.0, z: 3.0, a: 4.0}

f v = v.x +! v.y

r = f v1 +! f v2    -- this is valid

Swizzling

Swizzling means rearranging the elements of a vector.¹

(V3 1.0 2.0 3.0)%xxzy   ==   V4 1.0 1.0 3.0 2.0

The letters x, y, z and w refers to the 1st, 2nd, 3rd and 4th element of a record, respectively.
It is also possible to use the letters r, g, b and a instead of x, y, z and w.

Compositional typing

Compositional typing improves error messages.
Compositional typing can be seen as a language extension if we suppose that a language description provide information about ill-typed programs too.

Compositional typing does unification in a bottom-up order: during typing of expressions it unifies the calculated typings of subexpression. Doing so, compositional typing avoids the left-to-right (or right-to-left) bias caused by a substitution state carried by type inference algorithms used today.

As an example, consider the following code (example copied from Gergő Érdi’s thesis):

test x = (toUpper x, not x)

Gergő Érdi made a short survey on the error messages given some Haskell compilers:

• GHC 6.12: The subexpression toUpper x is processed first.

  Couldn’t match expected type ‘Bool’
  against inferred type ‘Char’
  In the first argument of ‘not’, namely ‘x’
  In the expression: not x
  In the expression: (toUpper x, not x)

• Hugs 98 seems to process application in the reversed order:

  ERROR "test.hs":1 - Type error in application
  *** Expression     : toUpper x
  *** Term           : x
  *** Type           : Bool
  *** Does not match : Char

• Helium 1.6 gives the same result as GHC above.

  (1,29): Type error in application
  expression     : not x
  function       : not
  type           : Bool -> Bool
  1st argument   : x
  type           : Char
  does not match : Bool

• Gergő Érdi’s prototype of compositional typing gives the following error message:

  input/test.hs:1:8-25:
  (toUpper x, not x)
  Cannot unify ‘Char’ with ‘Bool’ when unifying ‘x’:
        toUpper x    not x
        Char         Bool
  x ::  Char         Bool

Link to Gergő Érdi’s master thesis: Compositional Type Checking for Hindley-Milner Type Systems with Ad-hoc Polymorphism