Fakultas Ilmu Komputer UI

Skip to content
Snippets Groups Projects
Commit 44f8234a authored by Sean Gillespie's avatar Sean Gillespie Committed by GitHub
Browse files

Update system-f.md

Reword introduction
parent 92afbc2b
Branches
Tags
No related merge requests found
# System F # Introduction
System F is a typed variant of the Lambda Calculus. It is an extension to Pure λ can easily be extended with a static type system. We explore
another typed λ known as the Simply Typed Lambda Calculus. Additionally, two such systems, the *Simply Typed Lambda Calculus* and *System F*. The
System F introduces the concept of generic types, also called polymorphic Simply Typed Lambda Calculus, abbreviated as &lambda;<sub>&rarr;</sub> is
types [1]. the simplest typed &lambda;. *System F* is an extension of
&lambda;<sub>&rarr;</sub> that introduces the concept of generic types, also
called polymorphic types [1].
In general, type systems aim to eliminate certain programming errors [3]. A good In general, type systems aim to eliminate certain programming errors [3]. A good
type system should reject ill-typed programs, while not being too conservative-- type system should reject ill-typed programs, while accepting most valid programs
that is, it accepts most valid programs [2]. Many functional programming [2]. Many functional programming languages are based on type systems similar
languages are based on type systems similar to System F, including Haskell to System F, including Haskell (System FC [4]), and ML (Hindley-Milner [5]).
(System FC [4]), and ML (Hindley-Milner [5]).
# Type Context # Type Context
A typing context is a sequence mapping free variables to their types [2]. Given A typing context is a sequence mapping free variables to their types [2]. Given
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment