cmcl / frankjnr Goto Github PK

The compiler doesn't terminate type checking the following program.

The problem appears to arise from using the bound variable n which has type [ε]{Unit} as an argument to the constructor S.

on : {X -> {X -> Y} -> Y}
on x f = f x

interface Trivial = triv : Unit

data S = S { Unit }

interface State = get : S | put : S -> Unit

handleTrivial : <Trivial>X -> [State]X
handleTrivial x = x
handleTrivial <triv -> k> =
  on get! { (S n) -> put (S n); handleTrivial (k unit) }


main : { [Console]Unit }
main! = unit

The following fails to type check:

data Maybe X = just X | nothing

foo : Maybe {Unit} -> Unit
foo (just x) = x!

with the error:

 application:expected suspended computation, got: MkFTVar "X$f0"

It looks like x is being given a flexible type inside the body of foo when it should be given type {Unit}.

If I have a program without a definition for main but have a type signature then an error is triggered.

main : { [Console]Unit }  

frank: ppDef invariant broken: empty Def Exp detected.
CallStack (from HasCallStack):
  error, called at shonky/src/Shonky/Syntax.hs:182:24 in main:Shonky.Syntax

Hi,

Inspired by logSend in pipes.fk, I tried to write a logReceive, but hit an error. Here it is with the logging stripped out:

receivePassthrough : <Receive String>X -> [Receive String]X
receivePassthrough x              = x
receivePassthrough <receive -> r> = on receive! { s -> receivePassthrough (r s) }

The error I hit with that is

failed to unify abilities Receive ( List Char ) and

Should it work?

Sorry if this is a silly mistake!

Keep up the good work - frank is very exciting!

Chris

The following program is rejected with error "no main function defined.":

is_zero : Int -> Bool
is_zero i = i == 0

main : []Int
main! = is_zero 0

But the problem with this program is that the equality operator == is not defined in Frank.

The following program causes the Frank compiler not terminate:

data Bool = True | False

iffy : Bool -> {X} -> {X} -> X
iffy True t _  = t!
iffy False _ f = f!

main : Unit
main! = iffy True {1} {2}

... well, I don't know whether it eventually terminates. After 1 minute I gave up.

The existence of foo causes a unification failure.

data Zero =

interface Abort = aborting : Zero

data Bar = One {Int -> Int}

apply : Bar [Abort] -> Int -> [Abort]Int
apply (One f) x = f x

foo : Bar [Abort]
foo! = One {x -> x+1}

ex : Int -> [Abort]Int
ex n = apply foo! n

main : [Abort]Int
main! = ex 0

Inlining the definition of foo in the definition of ex gives
a program that passes the type checker and produces the desired
result (1).

This problem was originally identified by Jack Williams.

The following program triggers an error due to an incomplete pattern match. I haven't
dug into why yet. The crucial part is that Card is a datatype which contains a computation.

--- start of standard stuff ---
on : {X -> {X -> Y} -> Y}
on x f = f x

data S = S (List Card)  

data Card = Card { Unit }

interface State = get : S | put : S -> Unit

drawCardDeck : [State]Card
drawCardDeck! =
	on get! { (S (cons top deck)) -> put (S deck); top }

main : { [Console]Unit }
main! = unit

In an email with Craig, he pointed out a workaround to a problem I had been having.
Playing around with his workaround highlighted an inconsistency with how patterns are type checked.

In handleModifyPlayOrder, I can pattern match on MkEC and then use the effect polymorphic computation in an environment which has access to the State ability.

If I try to write a top level definition, not a handler, h, which does the same thing but does not handle an effect then the use of f is rejected.

on : X -> {X -> Y} -> Y
on x g = g x

interface ModifyOrder [E] = modifyOrder : EndoComp (List X) -> Unit

data EndoComp Y = MkEC {Y -> Y}

---
rotate : List X -> List X
rotate x = x

data S = S (List P)

interface State = get : S | put : S -> Unit

handleModifyPlayOrder : <ModifyOrder>X -> [State]X
handleModifyPlayOrder x = x
handleModifyPlayOrder <modifyOrder (MkEC f) -> k> =
  on get! { (S po) -> put (S (f po)); handleModifyPlayOrder (k unit) }

-- This doesn't type check
--h : EndoComp (List X) -> [State]Unit
--h (MkEC f) =
--  on get! { (S po) -> put (S (f po)) }

main : { [Console]Unit }
main! = unit

= Analysis

There seems to be an inconsistency about where makeFlexible is called.

In the first definition, the type checking first enters checkPat and then the case for MkCmdPat. Then crucially,
in the Just branch, makeFlexible is mapped over the types of the patterns. checkVPat is then called on each of the patterns with these flexible types.

In the second case, checkPat is called directly from checkCls which doesn't call makeFlexible on the result type which means the rigid type variable (X$r10) causes unification to fail.

This means that the arguments to checkVPat look like this, notice the subtle difference of MkRVar vs MkFVar.

For the handler:
Pattern Type: MkDTTy "EndoComp" [VArg (MkDTTy "List" [VArg (MkFTVar "X$f1")])
Args Type: EArg (MkAb (MkAbFVar "\163$f2") (fromList []))],[VArg (MkFTVar "Y$f3"),EArg (MkAb (MkAbFVar "\163$f4") (fromList []))])

For h:
Pattern Type: MkDTTy "EndoComp" [VArg (MkDTTy "List" [VArg (MkRTVar "X$r10")])
Args Type: EArg (MkAb (MkAbRVar "\163$r7") (fromList []))],[VArg (MkFTVar "Y$f0"),EArg (MkAb (MkAbFVar "\163$f1") (fromList []))])

This means we can't implement cooperative coroutining. The following is accepted:

interface Co = fork : {Unit} -> Unit
             | yield : Unit

but does not behave as expected - the computation argument to fork needs to be parameterised by an implicit ability argument. The rules for ability parameters (including implicit ones) should be just the same as for data types.