Skip to content

Instantly share code, notes, and snippets.

@gavinking
Last active February 7, 2018 09:42
Show Gist options
  • Star 2 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save gavinking/af1662a94c6d9690cfd8cc98cf1dcbbd to your computer and use it in GitHub Desktop.
Save gavinking/af1662a94c6d9690cfd8cc98cf1dcbbd to your computer and use it in GitHub Desktop.
Ceylon Web Runner: Records

Typesafe Records for Ceylon

The example demonstrates the use of Ceylon's powerful type system to define typesafe heterogenous maps, otherwise known as record types.

  • records.ceylon defines a tiny library for creating records
  • keys.ceylon defines example typesafe keys
  • test.ceylon is a runnable function demonstranting the use of the records library

Note that this code is experimental. Note also that due to bug #6602, it does not currently compile on the JVM.

//THREE TYPED KEYS
//Each key encodes the type of the item
//it is a key for, along with its own type
class Age extends Key<Age,Integer> {
shared new key extends Key<Age,Integer>() {}
}
class Name extends Key<Name,String> {
shared new key extends Key<Name,String>() {}
}
class Length extends Key<Length,Float> {
shared new key extends Key<Length,Float>() {}
}
module web_ide_script "1.0.0" {
// Add module imports here
}
"A record type, mapping a list of key types
to values. The type parameter [[U]] is a
union of key types."
sealed shared interface Record<U> {
//TODO: should really be contravariant,
// but there is a limitation in
// Ceylon's type arg inference that
// makes this impossible
shared formal I get<I>(Key<U,I> key);
}
"A key to an element in a [[Record]]. Keys
are singleton classes that extend this
class. The type parameter [[K]] encodes
the type of the key. The type parameter
[[I]] encodes the type of the keyed item."
abstract shared class Key<out K,I>() of K
given K satisfies Key<K,I> {}
"An empty [[Record]]."
shared Record<Nothing> emptyRecord
= EmptyRecord.instance;
"Create a record, given a [[key]] and [[item]]
and an existing [[record]]."
shared Record<U|K> record<U,K,I>
(Record<U> record, Key<K,I> key, I item)
given K satisfies Key<K,I>
=> ConsedRecord(record, key,item);
//INTERNAL IMPLEMENTATION
"An empty [[Record]]."
class EmptyRecord
satisfies Record<Nothing> {
shared actual I get<I>(Key<Nothing,I> key) {
assert (false);
}
shared new instance {}
}
"A [[Record]] composed of a key/item pair
and another record."
class ConsedRecord<U,K,T>
(Record<U> record, Key<K,T> key, T item)
satisfies Record<U|K>
given K satisfies Key<K,T> {
shared actual I get<I>(Key<U|K,I> key) {
if (key==this.key) {
assert (is I item = this.item);
return item;
}
else if (is Key<U,I> key) {
return record.get(key);
}
else {
assert (false);
}
}
}
shared void run() {
//EXAMPLE USAGE OF TYPESAFE RECORDS
//We form records by consing, beginning with
//the empty record:
value single = record(emptyRecord, Name.key, "Hello");
value pair = record(single, Age.key, 12);
value triple = record(pair, Length.key, 12.0);
//A record type like Record<Name|Age|Length>
//encodes the keys it will accept. Meanwhile,
//the key type itself encodes the type of its
//item. Thus, given a key, and a record, the
//item type pops out automatically:
Integer age = pair.get(Age.key);
String name = pair.get(Name.key);
print(age);
print(name);
Float length = triple.get(Length.key);
print(length);
//we can use use-site variance to abstract
//over all records that accept a certain
//key type or union of key types:
Record<in Age> ageOnly = triple;
Integer int = ageOnly.get(Age.key);
print(int);
Record<in Name|Length> nameAndLength = triple;
[String,Float] nameAndLengthAsPair
= [nameAndLength.get(Name.key),
nameAndLength.get(Length.key)];
print(nameAndLengthAsPair);
//UNSOUND THINGS THAT AREN'T ACCEPTED
//Record types are not covariant:
//Record<Name|Age|Length> rec = pair;
//get() only accepts keys that are
//defined for the given Record:
//pair.get(Length.key);
//We can't create a Record with an
//inconsistently-typed key/item pair:
//value sing = record(emptyRecord, Name.key, 12);
}
@gavinking
Copy link
Author

Click here to run this code online

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment