Jacques Garrigue garrigue
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* Encoding termination of a Turing machine into a GADT *) | |
| type s0 and s1 and s2 and s3 and s4 and fin | |
| type c0 and c1 and c2 and c3 and blank | |
| type left and right | |
| type endt | |
| type ('st_in, 'head_in, 'st_out, 'head_out, 'lr) transition = | |
| | Tr1 : (s0, 'a, s1, 'a, left) transition |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* Logic using GADTs *) | |
| exception Axiom | |
| type falso | |
| type ex_falso = {ex_falso: 'p. falso -> 'p} | |
| let ex_falso = {ex_falso = fun _ -> raise Axiom} | |
| type 'p not = 'p -> falso | |
| type ('a,'b) ior = Inl of 'a | Inr of 'b | |
| (* NB: the unit -> below is essential for soundness *) | |
| type classic = {classic: 'p. unit -> ('p, 'p not) ior} | |
| type (_,_) eq = Refl : ('x,'x) eq |