Upgrade to Pro
— share decks privately, control downloads, hide ads and more …
Speaker Deck
Sign up for free
Menu
Search
Features
All features
Private URLs
Password Protection
Custom URLS
Scheduled publishing
Remove Branding
Restrict embedding
Deck Collections
Notes
Features
All features
Private URLs
Password Protection
Custom URLS
Scheduled publishing
Remove Branding
Restrict embedding
Deck Collections
Notes
Explore
Featured decks
Featured speakers
Programming
Technology
Storyboards
Explore
Featured decks
Featured speakers
Programming
Technology
Storyboards
Pricing
Search
Sign in
Sign up for free
Compiling a Dependently Typed Language to Ruby
Search
Sponsored
·
Your Podcast. Everywhere. Effortlessly.
Share. Educate. Inspire. Entertain. You do you. We'll handle the rest.
→
Michael Bernstein
June 12, 2015
Programming
240
3
Share
Embed
Copy iframe code
Copy JS code
Copy link
Start on current slide
Compiling a Dependently Typed Language to Ruby
A.K.A. "Compilers Are Dope And Also A Little Bit About Fancy Types"
Michael Bernstein
June 12, 2015
More Decks by Michael Bernstein
See All by Michael Bernstein
I'd like to introduce you to a few of my closest friends
mrb
1
5k
Papers We Love NYC: "Propositions As Types" By Philip Wadler
mrb
1
1.8k
Programs That Eat Programs
mrb
2
1.4k
Know Your Types
mrb
5
3k
The Art of Obsession
mrb
3
910
The Research Omphalos
mrb
1
310
Papers We Love: "A Unified Theory of Garbage Collection"
mrb
4
2.3k
Distributed Systems Archaeology
mrb
22
3.2k
GoRuCo 2013
mrb
11
5.1k
Other Decks in Programming
See All in Programming
Spec-driven Development with AI
simas
PRO
0
2.2k
flutter_test のその先へ — Flutter アプリの LLM 機能に「評価」という品質保証を
kosukesaigusa
0
170
우리의 Nitro Modules는 당신의 Turbo Modules보다 아름답다
l2hyunwoo
0
250
Getting Started with Vibe Coding
miccheng
0
150
自作Discord音声botをLambda MicroVMsに移行した話 / Migrating My Discord Voice Bot to Lambda MicroVMs
akihisaikeda
1
240
sbt 2.0: takeoff
eed3si9n
0
190
Railsバージョンを4倍にした話
optim
0
900
AI駆動開発4年目の現在地(『あなたはFDEになるべきか?』イベント資料)
kumaiu
0
120
ChromeでローカルLLM
ryu1013
0
190
S3 TablesのIcebergデータに、AIエージェントからアクセスしてみた / 20261016developersio2026joetsu-accessing-iceberg-in-s3tables-via-agent
kasacchiful
PRO
0
250
学びを記事・スライド・Xへ高速展開する― AI-assisted Learning Loopで回すコンテンツ生成術
ochtum
0
180
Performance Optimization With LLMs
xleitix
0
230
Featured
See All Featured
Test your architecture with Archunit
thirion
2
2.5k
jQuery: Nuts, Bolts and Bling
dougneiner
66
8.7k
Ecommerce SEO: The Keys for Success Now & Beyond - #SERPConf2024
aleyda
1
2.2k
Designing Dashboards & Data Visualisations in Web Apps
destraynor
232
55k
CoffeeScript is Beautiful & I Never Want to Write Plain JavaScript Again
sstephenson
162
16k
We Are The Robots
honzajavorek
0
420
Digital Projects Gone Horribly Wrong (And the UX Pros Who Still Save the Day) - Dean Schuster
uxyall
1
3.7k
A Soul's Torment
seathinner
8
3.9k
Music & Morning Musume
bryan
48
7.5k
Put a Button on it: Removing Barriers to Going Fast.
kastner
60
4.6k
Odyssey Design
rkendrick25
PRO
2
910
RailsConf & Balkan Ruby 2019: The Past, Present, and Future of Rails at GitHub
eileencodes
141
35k
Transcript
Compiling A Dependently Typed Language To Ruby Michael R. Bernstein
RubyNation / 2015.6.12 / Silver Spring, Maryland
None
Why?
New ways of looking at how programs are designed, written,
executed, optimized, refactored, etc.
A New Lens
Compilers Are Dope And Also A Little Bit About Fancy
Types Michael R. Bernstein RubyNation / 2015.6.12 / Silver Spring, Maryland
None
None
None
None
Very Interesting
Why?
How?
Compilers
Compiler: - a computer program - that consumes computer programs
- and produces computer programs
Compiler: - a computer program - that does whatever you
want
[Animated image representing the sheer awesomeness of COMPILERS]
“Modern Compiler Implementation in ML” Appel
None
C ASM ????
X Y ????
Idris Ruby ????
Idris Ruby Rainbows, wizard dust, prayers, mystical insights, etc.
None
None
Intermediate Representations
None
Idris Ruby ????
LAMBDA CALCULUS
Everything that is computable can be expressed in terms of
the lambda calculus.
Everything that is computable can be compiled to the lambda
calculus.
Intermediate Representations Intermediate Representations Intermediate Representations Intermediate Representations Intermediate Representations
Intermediate Representations
TT TT Case IR Case IR Lift IR Defunc IR
ANF Idris ???
TT TT Case IR Case IR Lift IR Defunc IR
ANF Idris PHP
Tour and Demo!
None
DEEP BREATH
Type Systems
[Animated image representing the sheer awesomeness of TYPE SYSTEMS]
Dependent Types
Fancy Types
Expressive Types
pythag : Int -> List (Int, Int, Int) counter_rpc :
Int -> Maybe Int -> Process (Maybe Int) (Int,Int)
Program Phases
Syntax Check Compile Execute Test Type Check Write
Syntax Check Compile Execute Test Type Check Write
Syntax Check Compile Execute Test Type Check Write
More People To Read
Stephanie Weirich
Conor McBride
Philip Wadler
Works Cited
Sam Elliot, Edwin Brady, #idris, RubyNation & you! Acknowledgements
Thank You w michaelrbernste.in t @mrb_bk