search

mmirman / order

ordered logic thesis work
2 stars 1 forks source link

Linearity is not properly enforced #1

Closed liamoc closed 11 years ago

liamoc commented 11 years ago

This incorrectly typechecks:

test :: LL ((Top :-> Top) :-> (Top :-> Top) :-> Top :-> Top)
test = LL $ lam $ \f -> lam $ \g -> lam $ \y -> f # (f # y)

In other words, in the case where two variables have the same (linear) type, it does not ensure that both variables are used once, but instead ensures that either variable is used twice.

To fix this, simply remove the Rank-2 type from lam:

lam :: (rep h (Use a h) a -> rep (F a :+ hi) (U :+ ho) b) 
       -> rep hi ho (a :-> b)

There may be similar bugs elsewhere in your tagless class.

mmirman commented 11 years ago

I'm not really sure this fixes it as I don't remember how this code works since it is no longer related to my thesis. Are you sure this is a fix and doesn't introduce more bugs? I can see this trick being used in at least 2 other places and I can go change it if you are sure.

-Matt

liamoc commented 11 years ago

It seems to work for me. The goal is to ensure that the same variable is never used in two different contexts. Seeing as the context will be different after each use of a variable, this makes it impossible to use the same variable twice.

With the rank-2 type, the context h is specialised on each usage of the repeated variable to different contexts. Without the rank-2 type, the context h is global in scope and therefore there can only be one.

This does fix the problem, as far as I can tell. I'm not sure if the rest of it needs changes, I haven't examined it all in detail, just yet.

I found your trick most useful though as I am currently working on a linear-typed deeply-embedded DSL in Haskell for my work, so I needed an HOAS alternative to Oleg's de Bruijn encoding. Thanks for that.