Questions tagged [system-f]
19 questions
49
votes
1 answer
How did Haskell add Turing-completeness to System F?
I've been reading up on various type systems and lambda calculi, and i see that all of the typed lambda calculi in the lambda cube are strongly normalizing rather than Turing equivalent. This includes System F, the simply typed lambda calculus plus…
JwameeQohwiye
- 603
- 5
- 6
19
votes
1 answer
How to systematically compute the number of inhabitants of a given type?
How to systematically compute the number of inhabitants of a given type in System F?
Assuming the following restrictions:
All inhabitants terminate, i.e. no bottom.
All inhabitants lack side-effects.
For example (using Haskell syntax):
Bool has…
user1804599
11
votes
0 answers
Encoding universal types in terms of existential types?
In System F, the type exists a. P can be encoded as forall b. (forall a. P -> b) -> b in the sense that any System F term using an existential can be expressed in terms of this encoding respecting the typing and reduction rules.
In "Types and…
Agnishom Chattopadhyay
- 1,971
- 14
- 32
9
votes
2 answers
Example of type in System F that is not available in Hindley Milner type inference
Under 'What is Hindley Milner' it states:
Hindley-Milner is a restriction of System F, which allows more types but which requires annotations by the programmer.
My question is, What is an example of a type available in System F, that is not…
hawkeye
- 34,745
- 30
- 150
- 304
8
votes
1 answer
Characterizing the type of functions that can accept `()` as input (without monomorphizing)
Here are a few simple functions:
f1 :: () -> ()
f1 () = ()
f2 :: a -> a
f2 a = a
f3 :: a -> (a, a)
f3 a = (a, a)
f4 :: (a, b) -> a
f4 (a, b) = a
All of f1, f2, and f3 are able to accept () as an input. On the other hand, of course, f4 can't…
SEC
- 799
- 4
- 16
6
votes
2 answers
Type abstraction in GHC Haskell
I'd love to get the following example to type-check:
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
f :: Int ->…
Sebastian Graf
- 3,602
- 3
- 27
- 38
4
votes
1 answer
Haskell does-not want to type high rank polymorphism
I don't understand why this program is not typable :
type Test a = forall z. (a -> z) -> z
cons :: a -> Test a
cons = \a -> \p -> p a
type Identity = forall x. x -> x
t :: Identity
t = \x -> x
c :: Test Identity
c = cons (t :: Identity)
main ::…
abitbol
- 487
- 4
- 8
3
votes
1 answer
"Illegal polymorphic or qualified type" in instance declaration (System-F style trees)
I'm experimenting with implementing System-F-style data structures in Haskell.
I'll use A to mean application of a term A to a type B just to make it unambiguous (also using capitals for types).
Let's say Tree is the type of binary trees…
Oly
- 2,329
- 1
- 18
- 23
2
votes
0 answers
trouble encoding system f omega in final tagless in idris
so I am trying to do system f omega in final tagless style.
I had encoded system f successfully, as the following code (some example are also given)(also, please ignore the fact that inference is not working and the examples are very ugly, I will…
Marisa Kirisame
- 186
- 7
2
votes
1 answer
What is the canonical implementation of System F?
System F is a great way to simply reason about types when programming a prototype. Other than implementing it myself, I'd like to use an existing implementation.
When looking for implementations, there doesn't seem to be any - and I'm not sure why.…
hawkeye
- 34,745
- 30
- 150
- 304
2
votes
3 answers
What is required to extend an Untyped Lambda calculus implementation to cover the Simply Typed Lambda Calculus?
Matt Might talks about implementing a Lambda Calculus interpreter in 7 lines of Scheme:
; eval takes an expression and an environment to a value
(define (eval e env) (cond
((symbol? e) (cadr (assq e env)))
((eq? (car e) 'λ) (cons e env))
…
hawkeye
- 34,745
- 30
- 150
- 304
1
vote
1 answer
Can a type statically guarantee that a function to pairs only partially depends on its input?
Consider the type of a function from a's to pairs of b's and c's, a -> (b, c). (I'll use Haskell notation for types and functions, but this isn't a question about Haskell per se.) There are many such functions, including those where both, one, or…
SEC
- 799
- 4
- 16
1
vote
1 answer
System F Church numerals in Agda
I would like to test some definitions in system F using Agda as my typechecker and evaluator.
My first attempt to introduce Church natural numbers was by writing
Num = forall {x} -> (x -> x) -> (x -> x)
Which would be used just like a regular type…
radrow
- 6,419
- 4
- 26
- 53
1
vote
1 answer
Zip function in System F
Let's define list type
list = forall 'a, 'x. ('a -> 'x -> 'x) -> 'x -> 'x
where for instance
nil = Λ'a . Λ'x . λ(c : 'a -> 'x -> 'x) . λ(e : 'x) . e
cons = Λ'a . Λ'x . λ(head : 'a) . λ(tail : list 'a 'x) . λ(c : 'a -> 'x -> 'x) . λ(e : 'x) . c…
radrow
- 6,419
- 4
- 26
- 53
1
vote
1 answer
Haskell bind operator in System F including kinds
I need to know what is the System F type of the Haskell bind type (>>=) operator.
Until now I writed it like this:
(M::*->* A::*) -> (A::* -> (M::*->* B::*)) -> (M::*->* B:*)
Is it right? If it is right how do I find the final result?
Thank you!
yonutix
- 1,964
- 1
- 22
- 51