Skip to content

Commit 30a043a

Browse files
cstmlcstml
committed
update: comments
1 parent bd625e1 commit 30a043a

File tree

5 files changed

+114
-107
lines changed

5 files changed

+114
-107
lines changed

‎lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Derivation.hs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,6 @@ import Data.Map qualified as M
1717
import LambdaBuffers.Compiler.KindCheck.Kind (Kind)
1818
import LambdaBuffers.Compiler.KindCheck.Type (Type, Variable)
1919
import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess)
20-
2120
import Prettyprinter (
2221
Doc,
2322
Pretty (pretty),

‎lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs

Lines changed: 38 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -16,28 +16,34 @@ module LambdaBuffers.Compiler.KindCheck.Inference (
1616
Constraint (..),
1717
) where
1818

19+
import Control.Lens (view, (%~), (&), (.~), (^.))
1920
import Control.Monad.Freer (Eff, Member, Members, run)
2021
import Control.Monad.Freer.Error (Error, runError, throwError)
2122
import Control.Monad.Freer.Reader (Reader, ask, asks, local, runReader)
2223
import Control.Monad.Freer.State (State, evalState, get, put)
2324
import Control.Monad.Freer.Writer (Writer, runWriter, tell)
2425
import Data.Bifunctor (Bifunctor (second))
2526
import Data.Foldable (foldrM)
26-
import LambdaBuffers.Compiler.KindCheck.Derivation (Context (Context), Derivation (Abstraction, Application, Axiom, Implication), Judgement (Judgement), addContext, context, d'kind, d'type)
27+
import Data.Map qualified as M
28+
import Data.Text qualified as T
29+
import LambdaBuffers.Compiler.KindCheck.Derivation (
30+
Context (Context),
31+
Derivation (Abstraction, Application, Axiom, Implication),
32+
Judgement (Judgement),
33+
addContext,
34+
context,
35+
d'kind,
36+
d'type,
37+
)
2738
import LambdaBuffers.Compiler.KindCheck.Kind (Atom, Kind (KType, KVar, (:->:)))
28-
import LambdaBuffers.Compiler.KindCheck.Type (Type (Abs, App, Constructor, Opaque, Product, Sum, Var, VoidT), Variable (QualifiedTyRef, TyVar))
39+
import LambdaBuffers.Compiler.KindCheck.Type (
40+
Type (Abs, App, Constructor, Opaque, Product, Sum, UnitT, Var, VoidT),
41+
Variable (QualifiedTyRef, TyVar),
42+
)
2943
import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess, mkInfoLess)
30-
import Prettyprinter (Pretty (pretty), (<+>))
31-
32-
import Data.Text qualified as T
44+
import LambdaBuffers.Compiler.ProtoCompat.Types (localRef2ForeignRef)
3345
import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC
34-
35-
import Control.Lens (view, (%~), (&), (.~), (^.))
36-
import Data.Map qualified as M
37-
38-
import LambdaBuffers.Compiler.ProtoCompat.Types (
39-
localRef2ForeignRef,
40-
)
46+
import Prettyprinter (Pretty (pretty), (<+>))
4147

4248
-- | Utility to unify the two.
4349
getAllContext :: Context -> M.Map (InfoLess Variable) Kind
@@ -132,33 +138,23 @@ derive x = deriveTyAbs x
132138
pure a
133139

134140
deriveTyAbs :: PC.TyAbs -> Derive Derivation
135-
deriveTyAbs tyabs =
141+
deriveTyAbs tyabs = do
136142
case M.toList (tyabs ^. #tyArgs) of
137143
[] -> deriveTyBody (x ^. #tyBody)
138-
a@(n, _) : as -> do
139-
vK <- protoKind2Kind =<< getVarAnnotation tyabs n
140-
rK <- KVar <$> fresh
144+
a@(n, ar) : as -> do
145+
let argK = protoKind2Kind (ar ^. #argKind)
146+
bodyK <- KVar <$> fresh
141147
ctx <- ask
142148

143-
let newContext = ctx & addContext %~ (<> M.singleton (mkInfoLess (TyVar n)) vK)
149+
let newContext = ctx & addContext %~ (<> M.singleton (mkInfoLess (TyVar n)) argK)
144150
let newAbs = tyabs & #tyArgs .~ uncurry M.singleton a
145151
let restAbs = tyabs & #tyArgs .~ M.fromList as
146152

147153
restF <- local (const newContext) $ deriveTyAbs restAbs
148154

149155
let uK = restF ^. d'kind
150-
tell [Constraint (rK, uK)]
151-
pure $ Abstraction (Judgement ctx (Abs newAbs) (vK :->: rK)) restF
152-
153-
-- Convert from internal Kind to Proto Kind.
154-
protoKind2Kind :: PC.Kind -> Derive Kind
155-
protoKind2Kind = \case
156-
PC.Kind k -> case k of
157-
PC.KindArrow k1 k2 -> (:->:) <$> protoKind2Kind k1 <*> protoKind2Kind k2
158-
PC.KindRef PC.KType -> pure KType
159-
PC.KindRef PC.KUnspecified -> KVar <$> fresh -- unspecified kinds get inferred and unified
160-
getVarAnnotation :: PC.TyAbs -> PC.VarName -> Derive PC.Kind
161-
getVarAnnotation tyabs varname = pure $ ((tyabs ^. #tyArgs) M.! varname) ^. #argKind
156+
tell [Constraint (bodyK, uK)]
157+
pure $ Abstraction (Judgement ctx (Abs newAbs) (argK :->: bodyK)) restF
162158

163159
deriveTyBody :: PC.TyBody -> Derive Derivation
164160
deriveTyBody = \case
@@ -191,7 +187,7 @@ derive x = deriveTyAbs x
191187
deriveRecord :: PC.Record -> Derive Derivation
192188
deriveRecord r = do
193189
case M.toList (r ^. #fields) of
194-
[] -> voidDerivation
190+
[] -> unitDerivation
195191
f : fs -> do
196192
d1 <- deriveField $ snd f
197193
d2 <- deriveRecord $ r & #fields .~ M.fromList fs
@@ -240,9 +236,10 @@ derive x = deriveTyAbs x
240236
foldrM productDerivation voidD ds
241237

242238
voidDerivation :: Derive Derivation
243-
voidDerivation = do
244-
ctx <- ask
245-
pure $ Axiom $ Judgement ctx VoidT KType
239+
voidDerivation = (\ctx -> Axiom $ Judgement ctx VoidT KType) <$> ask
240+
241+
unitDerivation :: Derive Derivation
242+
unitDerivation = (\ctx -> Axiom $ Judgement ctx UnitT KType) <$> ask
246243

247244
productDerivation :: Derivation -> Derivation -> Derive Derivation
248245
productDerivation d1 d2 = do
@@ -380,3 +377,11 @@ substitute s d = case d of
380377
-- | Fresh startAtom
381378
startAtom :: Atom
382379
startAtom = 0
380+
381+
-- Convert from internal Kind to Proto Kind.
382+
protoKind2Kind :: PC.Kind -> Kind
383+
protoKind2Kind = \case
384+
PC.Kind k -> case k of
385+
PC.KindArrow k1 k2 -> protoKind2Kind k1 :->: protoKind2Kind k2
386+
PC.KindRef PC.KType -> KType
387+
PC.KindRef PC.KUnspecified -> KType -- unspecified kinds get inferred and unified

‎lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,9 @@ import Prettyprinter (Pretty (pretty), viaShow)
1515
import Test.QuickCheck (Arbitrary)
1616
import Test.QuickCheck.Arbitrary.Generic (GenericArbitrary (GenericArbitrary))
1717

18+
-- NOTE(cstml): Let's remove the Arbitrary instances and replaces them with
19+
-- Gens.
20+
1821
data Variable
1922
= -- | All TyRefs are fully qualified. The context determines if they're local
2023
-- or not.

‎lambda-buffers-proto/compiler-proto.md

Lines changed: 70 additions & 67 deletions
Original file line numberDiff line numberDiff line change
@@ -18,10 +18,11 @@
1818
- [Kind](#lambdabuffers-compiler-Kind)
1919
- [Kind.KindArrow](#lambdabuffers-compiler-Kind-KindArrow)
2020
- [KindCheckError](#lambdabuffers-compiler-KindCheckError)
21-
- [KindCheckError.ImpossibleUnificationError](#lambdabuffers-compiler-KindCheckError-ImpossibleUnificationError)
21+
- [KindCheckError.CyclicKindError](#lambdabuffers-compiler-KindCheckError-CyclicKindError)
2222
- [KindCheckError.InconsistentTypeError](#lambdabuffers-compiler-KindCheckError-InconsistentTypeError)
23-
- [KindCheckError.RecursiveKindError](#lambdabuffers-compiler-KindCheckError-RecursiveKindError)
24-
- [KindCheckError.UnboundTermError](#lambdabuffers-compiler-KindCheckError-UnboundTermError)
23+
- [KindCheckError.UnboundTyRefError](#lambdabuffers-compiler-KindCheckError-UnboundTyRefError)
24+
- [KindCheckError.UnboundTyVarError](#lambdabuffers-compiler-KindCheckError-UnboundTyVarError)
25+
- [KindCheckError.UnificationError](#lambdabuffers-compiler-KindCheckError-UnificationError)
2526
- [Module](#lambdabuffers-compiler-Module)
2627
- [ModuleName](#lambdabuffers-compiler-ModuleName)
2728
- [ModuleNamePart](#lambdabuffers-compiler-ModuleNamePart)
@@ -61,9 +62,9 @@
6162
- [TyVar](#lambdabuffers-compiler-TyVar)
6263
- [Tys](#lambdabuffers-compiler-Tys)
6364
- [VarName](#lambdabuffers-compiler-VarName)
64-
65+
6566
- [Kind.KindRef](#lambdabuffers-compiler-Kind-KindRef)
66-
67+
6768
- [Scalar Value Types](#scalar-value-types)
6869

6970

@@ -191,34 +192,6 @@ Compiler Result ~ a successful Compilation Output.
191192

192193

193194

194-
<a name="lambdabuffers-compiler-CompilerOutput"></a>
195-
196-
### CompilerOutput
197-
Output of the Compiler.
198-
199-
200-
| Field | Type | Label | Description |
201-
| ----- | ---- | ----- | ----------- |
202-
| compilation_error | [CompilerError](#lambdabuffers-compiler-CompilerError) | | |
203-
| compilation_result | [CompilerResult](#lambdabuffers-compiler-CompilerResult) | | |
204-
205-
206-
207-
208-
209-
210-
<a name="lambdabuffers-compiler-CompilerResult"></a>
211-
212-
### CompilerResult
213-
Compiler Result ~ a successful Compilation Output.
214-
215-
equivalent of unit.
216-
217-
218-
219-
220-
221-
222195
<a name="lambdabuffers-compiler-ConstrName"></a>
223196

224197
### ConstrName
@@ -348,34 +321,39 @@ Kind checking errors.
348321

349322
| Field | Type | Label | Description |
350323
| ----- | ---- | ----- | ----------- |
351-
| unbound_term_error | [KindCheckError.UnboundTermError](#lambdabuffers-compiler-KindCheckError-UnboundTermError) | | |
352-
| unification_error | [KindCheckError.ImpossibleUnificationError](#lambdabuffers-compiler-KindCheckError-ImpossibleUnificationError) | | |
353-
| recursive_subs_error | [KindCheckError.RecursiveKindError](#lambdabuffers-compiler-KindCheckError-RecursiveKindError) | | |
324+
| unbound_ty_ref_error | [KindCheckError.UnboundTyRefError](#lambdabuffers-compiler-KindCheckError-UnboundTyRefError) | | |
325+
| unbound_ty_var_error | [KindCheckError.UnboundTyVarError](#lambdabuffers-compiler-KindCheckError-UnboundTyVarError) | | |
326+
| unification_error | [KindCheckError.UnificationError](#lambdabuffers-compiler-KindCheckError-UnificationError) | | |
327+
| cyclic_kind_error | [KindCheckError.CyclicKindError](#lambdabuffers-compiler-KindCheckError-CyclicKindError) | | |
354328
| inconsistent_type_error | [KindCheckError.InconsistentTypeError](#lambdabuffers-compiler-KindCheckError-InconsistentTypeError) | | |
355329

356330

357331

358332

359333

360334

361-
<a name="lambdabuffers-compiler-KindCheckError-ImpossibleUnificationError"></a>
335+
<a name="lambdabuffers-compiler-KindCheckError-CyclicKindError"></a>
362336

363-
### KindCheckError.ImpossibleUnificationError
364-
Unification has failed - type is incorrectly defined. Error reads as
365-
follows:
366-
&gt; In ty_name definition an error has occurred when trying to unify kind
367-
&gt; ty_kind_1 with ty_kind_2.
337+
### KindCheckError.CyclicKindError
338+
A cyclic kind was encountered. Infinite kinds like this are not acceptable,
339+
and we do not support them. We could not construct infinite kind in ty_def.
368340

369-
FIXME(cstml): add source of constraint to the error such that user can see
370-
where the constraint was generated - therefore where the error precisely
371-
is.
341+
As the implementation currently stands such an error is (most likely) not
342+
representable - therefore not reachable. Such an error would usually occur
343+
for a term like: λa. a a - in which case the inference would try to unify
344+
two kinds of the form: m and m -&gt; n - because m appears in both terms -
345+
the cyclic unification error would be thrown.
346+
347+
In the case of LambdaBuffers - such an error is not (currently) achievable
348+
as the kind of the variable is given by the context - (i.e. λa : m . a a,
349+
where m is a kind) therefore the unification would fail with Unification
350+
Error. Nevertheless - future features might require it.
372351

373352

374353
| Field | Type | Label | Description |
375354
| ----- | ---- | ----- | ----------- |
376-
| ty_name | [TyName](#lambdabuffers-compiler-TyName) | | |
377-
| ty_kind_1 | [Kind](#lambdabuffers-compiler-Kind) | | |
378-
| ty_kind_2 | [Kind](#lambdabuffers-compiler-Kind) | | |
355+
| ty_def | [TyDef](#lambdabuffers-compiler-TyDef) | | |
356+
| module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | |
379357

380358

381359

@@ -385,46 +363,72 @@ is.
385363
<a name="lambdabuffers-compiler-KindCheckError-InconsistentTypeError"></a>
386364

387365
### KindCheckError.InconsistentTypeError
388-
The inferred type differs from the type as defined.
366+
The actual_kind differs from the expected_kind.
367+
368+
369+
| Field | Type | Label | Description |
370+
| ----- | ---- | ----- | ----------- |
371+
| module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | |
372+
| ty_def | [TyDef](#lambdabuffers-compiler-TyDef) | | |
373+
| actual_kind | [Kind](#lambdabuffers-compiler-Kind) | | |
374+
| expected_kind | [Kind](#lambdabuffers-compiler-Kind) | | |
375+
376+
377+
378+
379+
380+
381+
<a name="lambdabuffers-compiler-KindCheckError-UnboundTyRefError"></a>
382+
383+
### KindCheckError.UnboundTyRefError
384+
Unbound type reference ty_ref detected in term ty_def.
389385

390386

391387
| Field | Type | Label | Description |
392388
| ----- | ---- | ----- | ----------- |
393-
| ty_name | [TyName](#lambdabuffers-compiler-TyName) | | |
394-
| inferred_kind | [Kind](#lambdabuffers-compiler-Kind) | | |
395-
| defined_kind | [Kind](#lambdabuffers-compiler-Kind) | | |
389+
| module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | |
390+
| ty_def | [TyDef](#lambdabuffers-compiler-TyDef) | | |
391+
| ty_ref | [TyRef](#lambdabuffers-compiler-TyRef) | | |
396392

397393

398394

399395

400396

401397

402-
<a name="lambdabuffers-compiler-KindCheckError-RecursiveKindError"></a>
398+
<a name="lambdabuffers-compiler-KindCheckError-UnboundTyVarError"></a>
403399

404-
### KindCheckError.RecursiveKindError
405-
Inifinitely recursive term detected in definition ty_name.
400+
### KindCheckError.UnboundTyVarError
401+
Unbound variable ty_var detected in term ty_def.
406402

407403

408404
| Field | Type | Label | Description |
409405
| ----- | ---- | ----- | ----------- |
410-
| ty_name | [TyName](#lambdabuffers-compiler-TyName) | | |
406+
| module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | |
407+
| ty_def | [TyDef](#lambdabuffers-compiler-TyDef) | | |
408+
| ty_var | [TyVar](#lambdabuffers-compiler-TyVar) | | |
409+
411410

412411

413412

414413

415414

415+
<a name="lambdabuffers-compiler-KindCheckError-UnificationError"></a>
416416

417-
<a name="lambdabuffers-compiler-KindCheckError-UnboundTermError"></a>
417+
### KindCheckError.UnificationError
418+
In ty_def an error has occurred when trying to unify kind ty_kind_lhs
419+
with ty_kind_rhs.
418420

419-
### KindCheckError.UnboundTermError
420-
Error referring to an unbound term. This usually means that the term was
421-
not defined.
421+
FIXME(cstml): Add source of constraint to the error such that user can see
422+
where the constraint was generated - therefore where the error precisely
423+
is.
422424

423425

424426
| Field | Type | Label | Description |
425427
| ----- | ---- | ----- | ----------- |
426-
| ty_name | [TyName](#lambdabuffers-compiler-TyName) | | |
427-
| var_name | [VarName](#lambdabuffers-compiler-VarName) | | |
428+
| module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | |
429+
| ty_def | [TyDef](#lambdabuffers-compiler-TyDef) | | |
430+
| ty_kind_lhs | [Kind](#lambdabuffers-compiler-Kind) | | |
431+
| ty_kind_rhs | [Kind](#lambdabuffers-compiler-Kind) | | |
428432

429433

430434

@@ -1163,7 +1167,6 @@ Type variable
11631167
| Field | Type | Label | Description |
11641168
| ----- | ---- | ----- | ----------- |
11651169
| var_name | [VarName](#lambdabuffers-compiler-VarName) | | Variable name. |
1166-
| source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. |
11671170

11681171

11691172

@@ -1200,7 +1203,7 @@ Type variable name
12001203

12011204

12021205

1203-
1206+
12041207

12051208

12061209
<a name="lambdabuffers-compiler-Kind-KindRef"></a>
@@ -1214,11 +1217,11 @@ A built-in kind.
12141217
| KIND_REF_TYPE | 1 | A `Type` kind (also know as `*` in Haskell) built-in. |
12151218

12161219

1220+
12171221

1222+
12181223

1219-
1220-
1221-
1224+
12221225

12231226

12241227

‎lambda-buffers-proto/run.sh

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,3 @@
1-
function gen-compiler-docs {
2-
protoc --plugin=`which protoc-gen-doc` compiler.proto --doc_out=. --doc_opt=markdown,compiler-proto.md
3-
echo "<!-- markdownlint-disable-file -->" >> compiler-proto.md
4-
}
5-
6-
gen-compiler-docs
1+
#!/bin/sh
2+
protoc --plugin=`which protoc-gen-doc` compiler.proto --doc_out=. --doc_opt=markdown,compiler-proto.md
3+
echo "<!-- markdownlint-disable-file -->" >> compiler-proto.md

0 commit comments

Comments
 (0)