For example:

Trying to use an anonymous type function (higher order functions are not supported yet)

module Test with letrec id [a : Data] (x : a) : a = x foo (_ : Unit) : Unit = do id (/\a. \(x : a). x) () Fragment violation when converting Tetra module to Salt module. Cannot convert expression. Cannot convert type abstraction in this context. The program must be lambda-lifted before conversion. with: /\(a : Data). \(x : a). x

Trying to use higher kinded type arguments (which need an 'Any' region to implement safely, in general)

module Test data List (a : Data) where Nil : a -> List a Cons : a -> List a -> List a with letrec foo [a : Data ~> Data] [b : Data] (x : b) : b = x bar (_ : Unit) : Nat# = foo [List] [Nat#] 5# Cannot convert expression. Unsupported type argument to function or constructor. In particular, we don't yet handle higher kinded type arguments. See [Note: Salt conversion for higher kinded type arguments] in the implementation of the Tetra to Salt conversion. with: [List]

Trying to partially apply a primitive operator:

module Test with letrec thing (_ : Unit) : Nat# -> Nat# = add# [Nat#] 5# Fragment violation when converting Tetra module to Salt module. Cannot convert expression. Partial application of primitive operators is not supported. with: add# [Nat#] 5#

In contrast, the old ddc-alpha compiler (which I wrote for my PhD work), would signal its displeasure with partially applied primops by producing a program that segfaulted at runtime. We turn our backs on the bad old days.

### Nested Data Types

Pleasingly, the new type inferencer does seem to work with some non-standard programs -- even though these don't compile all the way to object code yet. Here is a Core Tetra program using nested data types:module Test data Tuple2 (a b : Data) where T2 : a -> b -> Tuple2 a b data Nest (a : Data) where NilN : Nest a ConsN : a -> Nest (Tuple2 a a) -> Nest a with letrec thing (_ : Unit) = ConsN 7# (ConsN (T2 1# 2#) (ConsN (T2 (T2 6# 7#) (T2 7# 4#)) NilN))This example is based on one from the Bird and Meertens 1998 paper. Note that the second argument of the ConsN constructor takes a Nest where the element type is more complex than the original parameter. The type inference algorithm in the alpha compiler would have diverged on this program.

### Higher Rank Types

I've also tried out some simple examples with higher ranked types, here is one:module Test with letrec thing1 (blerk : ([a : Data]. a -> a) -> Nat#) : Nat# = blerk (/\a. \(x : a). x) thing2 (u : Unit) = thing1 (\(f : [a : Data]. a -> a). f 5#)thing1 has a rank-3 type because it is a function, that takes a function, that takes a function which is polymorphic. There is a quantifier that appears at depth 3 contravariantly. Writing the type of thing1 in full makes this easier to see:

thing1 :: ((([a : Data]. a -> a) -> Nat#) -> Nat#Again, I can't compile this example to object code yet because code generation for higher order functions isn't finished. However, type inference is a separate concern, and I don't know of any remaining problems in this part.

## No comments:

## Post a Comment