-
Notifications
You must be signed in to change notification settings - Fork 0
/
typed.py
128 lines (79 loc) · 2.47 KB
/
typed.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
from __future__ import annotations
import dataclasses
import typing
from typing import TypeAlias
@dataclasses.dataclass(frozen=True)
class TCon:
id: str
kind: Kind
alts: list[str] = dataclasses.field(default_factory=list)
def w(self) -> Type:
return self
def __repr__(self) -> str:
return f"{self.id}"
@dataclasses.dataclass(frozen=True)
class TVar:
id: int
kind: Kind
def __repr__(self) -> str:
return f"@{self.id}"
@dataclasses.dataclass
class TAp:
con: Type
arg: Type
def __repr__(self) -> str:
match self.con:
case TCon("Array"):
return f"[{self.arg}]"
case TAp(TCon("Callable"), TAp() as arg):
return f"({arg!r}) -> {self.arg}"
case TAp(TCon("Callable"), arg):
return f"{arg!r} -> {self.arg}"
return f"{self.con!r}<{self.arg!r}>".replace("><", ", ")
Type: TypeAlias = TVar | TCon | TAp
@dataclasses.dataclass
class KStar:
pass
def w(self) -> Kind:
return self
@dataclasses.dataclass
class KFun:
arg: Kind
ret: Kind
Kind: TypeAlias = KStar | KFun
TUnit = TCon("Unit", KStar())
TRegex = TCon("Regex", KStar())
TStr = TCon("Str", KStar())
TNum = TCon("Num", KStar())
TFloat = TCon("Float", KStar())
TTupleCon = TCon("Tuple", KFun(KStar(), KFun(KStar(), KStar())))
def pair(a: Type, b: Type) -> TAp:
return TAp(TAp(TTupleCon, a), b)
TCallableCon = TCon("Callable", KFun(KStar(), KFun(KStar(), KStar())))
def TDef(arg: Type, ret: Type) -> TAp:
return TAp(TAp(TCallableCon, arg), ret)
TArrayCon = TCon("Array", KFun(KStar(), KStar()))
def TArray(t: Type) -> TAp:
return TAp(TArrayCon, t)
SomeCon = TCon("Some", KFun(KStar(), KStar()))
NoneCon = TCon("None", KStar())
TOptionCon = TCon("Option", KFun(KStar(), KStar()), [SomeCon.id, NoneCon.id])
def TOption(t: Type) -> TAp:
return TAp(TOptionCon, t)
TrueCon = TCon("True", KStar())
FalseCon = TCon("False", KStar())
TBool = TCon("Bool", KStar(), [TrueCon.id, FalseCon.id])
def kind(t: Type) -> Kind:
match t:
case TVar(_, k):
return k
case TCon(_, k):
return k
case TAp(arg):
match kind(arg):
case KFun(_, k):
return k
raise TypeError(f"kind of {t}")
def assert_never(value: typing.NoReturn) -> typing.NoReturn:
# This also works at runtime as well
assert False, f"This code should never be reached, got: {value}"