PHI 11 - Type Constructors #13
Conversation
Merges in content from PHI 5 (type variables) with latex judgements for bidirectional type elaboration and kind synthesis/analysis. Will follow up with content from the PHI 3 (type aliases) later.
need to make a TypeEquiv^ and a TypeEquivv
except the rules are obnoxiously opaque and derivations tediously convuluted
now there's \rule, \rinfer, \rrule, \inferrule...
too tired to check
fiddled around w/ latex for a long time this doc is really quite a mess
|
|
||
| ## Introduction | ||
|
|
||
| see my SURE poster for a motivating example. |
| @@ -0,0 +1,699 @@ | |||
| \ProvidesClass{joshuadunfield}[2015/06/20 - Minor revision] | |||
There was a problem hiding this comment.
jana dunfield no longer goes by joshua so let's rename this style file
| @@ -0,0 +1,920 @@ | |||
| %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |||
There was a problem hiding this comment.
there are two 11-type-constructors.tex files, one here and one in the parent directory. which one am I reviewing? please consolidate.
There was a problem hiding this comment.
(I was using the upper .tex to generate the .md phi information)
I've been getting problems w/ \newcommand{\mathcolor}{..} redefinition
in this file recently (w/ the old 2015 version).
How did this ever compile? Something upstream with amsmath or something
must've changed since none of the previous commits build
I swear it worked before though
| @@ -0,0 +1,13 @@ | |||
| \documentclass[12pt]{article} | |||
There was a problem hiding this comment.
this file should be deleted I think.
There was a problem hiding this comment.
It's to generate the markdown file
I can delete it since it seems like it's confusing
| | Π TID Knd Knd | ||
| deriving (Show) | ||
|
|
||
| -- I'm afraid that sooner or later I'll run into a case where just using De |
There was a problem hiding this comment.
why didn't you use de Bruijn indices? (that's what we're doing in the Hazel implementation)
There was a problem hiding this comment.
At the time, I thought:
-- the phi uses variable names, so the implementation might as well too to make sure the renaming rules are right
-- it might be easier to debug w/o de Bruijn indices
-- I was going to use a Barendregt convention anyways, so it should be a little easier to implement
(of course the third point doesn't actually make sense, and is somewhat opposed to the first)
I agree in retrospect that I should've done de Bruijn indices like you'd said at the beginning, but I was still learning these things and wrote all the renaming stuff early on
Now there's not much point in changing it in the haskell implementation right?
| | Ctx :⌢⌢⌢ EAssump | ||
| deriving (Show) | ||
|
|
||
| -- TODO: this is c/p from ECtx |
There was a problem hiding this comment.
what is this TODO saying? that the external and internal languages are the same?
There was a problem hiding this comment.
yeah that the external and internal type level languages are the same, but the internal language should have kind casts
| -- The internal type language | ||
| -- (following ``convention'', we speak of terms and types, not types and kinds | ||
| -- in the context of normalization) | ||
| -- TODO: In the future, should contain kind casts for a full gradual |
There was a problem hiding this comment.
what can't currently be expressed?
There was a problem hiding this comment.
if you write something like
type T = Int in
type V = λt::KHole.t Bool in
type Bogus = V T in
...
kind casts would let you express why Bogus is bogus
| False | ||
| , Nil ⊢ tequiv (Tλ "t" Type $ TVar "t") (Tλ "t" Type Bse) Type ~?= False | ||
| , Nil ⊢ | ||
| tequiv (Tλ "t" Type $ TVar "t") (Tλ "t" Type Bse) (Π "t" Type Type) ~?= |
There was a problem hiding this comment.
"t" isn't in scope in the annotation on Tλ right?
There was a problem hiding this comment.
Yes, although I'm confused what that has to do with those tests?
| -- tequiv τ1 τ2 κ = \aΓ -> Algo.tequiv aΓ τ1 τ2 κ | ||
| -- since application precedence is so high (and can't be competed against) | ||
| tequiv :: _ | ||
| tequiv = ((.) . (.) $ flip) . ((.) flip) . flip $ Algo.tequiv |
There was a problem hiding this comment.
I just wanted to try to rearrange the arguments point free/with combinators. To see if I could do it.
…reason and I'm really not in the mood to try to fix it right now when I can't even seem to build it from source and yes I'm annoyed right now
No description provided.