Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Twelf seems very finicky about certain details. Here I explore how associative lists depend in unreasonable ways on the complexity of the value type.
% Testing how lookup in an associative list works.
% We consider associative lists with keys of type key and values
% of type value.
%
% Ideally, we want key to be any type with decidable
% equality and value to be any type. However, we use natural numbers
% as keys so that we can convince Twelf that key has decidable equality.
% Is there a way to tell Twelf "assume key has decidable equality"?
%
% Even more annoyingly, code breaks depending on how complicated
% the type of values is. If we keep value abstract, it works.
% If we make value = a -> b for some types a and b, then it works.
% But if we make value = (a -> b) -> a then it stops working, unless
% we add a worlds declaration for a, or make a wrapper type, see below.
% Booleans, so we can compare stuff.
bool : type.
true : bool.
false : bool.
% We use natural numbers as keys. We would prefer to hypothesise a
% type with decidable equality, but how can we do that in Twelf?
key : type.
z : key.
s : key -> key.
% Auxiliary types, just to have something to play with.
a : type.
b : type.
dog : a -> b.
cat : b -> a.
% We are interested in the case when the values are functions.
% We present three options here. Why do some work and others not?
% OPTION I (works)
% %abbrev value = a -> b.
% OPTION II (does not work)
% %abbrev value = (a -> b) -> a.
% OPTION III (works)
% Add a worlds declaration for a and b.
% %worlds () (a) (b).
% %abbrev value = (a -> b) -> a.
% OPTION IV (works)
% Wrap (a -> b) -> a in a constructor
value : type.
value/make : ((a -> b) -> a) -> value.
%block key-var : block {k : key}.
%block value-var : block {v : value}.
% Associative lists holding (key, value) pairs
list : type.
nil : list.
cons : key -> value -> list -> list.
% Equality of keys is decidable.
key-equal : key -> key -> bool -> type.
%mode key-equal +K +K' -B.
key-equal/zz : key-equal z z true.
key-equal/zs : key-equal z (s _) false.
key-equal/sz : key-equal (s _) z false.
key-equal/ss : key-equal (s K) (s K') B <- key-equal K K' B.
%worlds () (key-equal _ _ _).
%total {K K'} (key-equal K K' _).
if-then-else : bool -> value -> value -> value -> type.
%mode if-then-else +B +V1 +V2 -V.
- : if-then-else true V _ V.
- : if-then-else false _ V V.
%worlds () (if-then-else _ _ _ _).
%total {B} (if-then-else B _ _ _).
% Finally, here is lookup in an associative array,
% with default value if key not found.
lookup : key -> list -> value -> value -> type.
%mode lookup +Key +List +Default -Value.
lookup/nil : lookup K nil D D.
lookup/cons : lookup K (cons K' V L) D V''
<- lookup K L D V'
<- key-equal K K' B
<- if-then-else B V V' V''.
%worlds () (lookup _ _ _ _).
%total {L} (lookup _ L _ _).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.