meowrobot changed the topic of #elliottcable to: Your topic makes my IRC client cry. π―ππ-ππ-π―πππππππππ-π―ππππππ || #ELLIOTTCABLEΒ is not about ELLIOTTC [string lost in sudden transmission termination]
<drparse>
disagree
<drparse>
people transpile to JS because they have no choice
<drparse>
JS is the only language allowed in browsers
<drparse>
people want to use other languages, other syntaxes, etc
<drparse>
until asm.js is mature, transpilers are absolutely valid
<jfhbrook>
are you at least trying to help in ##javascript ?
<jfhbrook>
I don't hang out there cause I don't do client side work
<ec>
TypeScript isn't a new language, though
<ec>
it
<ec>
is attempting to be JavaScript-y
<ec>
in which case: just do it the *right way*
<ec>
i.e. on top of JavaScript
<ec>
check out flow. it's great.
<drparse>
nah
<ec>
they both have the same failing tho. no hkt.
<ec>
god so much trash in my old Droplr
<drparse>
ec: another reason to not use constraints!
<drparse>
hkt is a god damn phd thesis to implement with constraints
<drparse>
so we have to start off with intrinsic types, e.g. Bool, but let's add a dollar sign so we can tell the difference between those and type aliases $Bool
<jfhbrook>
that sounds annoying
<drparse>
this is just for description
<jfhbrook>
python would never stand for dollar signs!
<drparse>
:(
<drparse>
:C
<drparse>
then write Bool = $Bool lol
<drparse>
so it's important to make a distinction between type representations and type expressions
<drparse>
a type expression is evaluated to produce a type representation
<drparse>
like if you have Foo = $Int, then the expression `Foo` is evaluated to produce `$Int`
<drparse>
I just want the representations
<drparse>
oh also you have to distinguish between type predicates and types
<drparse>
e.g. "conforms to interface X" is not a type
<drparse>
it's a type predicate
<drparse>
e.g. you might want to write a function next(Iterator<T>) -> T?
<drparse>
but if Iterator is an interface
<drparse>
then really you're doing
<drparse>
next<A>(A) -> (A.Iteree)? where (A implements Iterator)
<drparse>
erm not Iteree is the wrong name, but you get the idea
<drparse>
so Iterator is not a type
<drparse>
the things that DO end up being types are: primatives, record types, function types, ...
<drparse>
and we need some notion of associated types
<drparse>
record type is easy, just { label1: TypeA, label2: TypeB, ... }
<drparse>
function types are more interesting
<drparse>
presumably there should be some interface (or interfaces) for function types, but as above interfaces are not types!
<drparse>
for the actual type representations, you want some kind of structure of types (not to be confused with a record type). which also satisfies our requirement for associated types. although I don't know how this works with covariance/contravariance
<drparse>
like you can think of a function as being a type structure { Input: Type, Output: Type }
<drparse>
maybe covariance/contravariance could be part of the type of the type (kind?)
<drparse>
I think it's interesting how a double layer type system ends up being the best
<drparse>
like all sufficiently powerful type systems tend towards having types of types
<drparse>
but is there any use for having types of types of types? I think not
<drparse>
probably because the type checker is a program that runs at compile-time, so the types are objects in that program and the expression in that program can be type-checked, but because language of types is interpreted it's not useful to have more layers than that
<drparse>
Array = { Of: Type }
<drparse>
Dict = { Key: Type, Val: Type }
<drparse>
Set = \T -> Dict{ Key: T, Val: $Void }
<drparse>
HasLength = \T -> $methodMatching( length :: T -> Int )
<drparse>
so this is okaaaay
<drparse>
ok you kind of want named arguments
<drparse>
then you have maps between type structures
<drparse>
like
<drparse>
Set = \{ Of: Type } -> Dict{ Key: T, Val: $Void }
<drparse>
then if you use the same notation...
<drparse>
Set { Of: Int }
<drparse>
Dict { Key: Int, Val: $Void }
<drparse>
that is nice
<drparse>
Record = { Fields: [(Ident, Type)] } lol records just don't fit at all
<drparse>
I guess you also want to be able to access the type of a record field by label
<drparse>
foo<T>(...) where T.label1 is Int
<drparse>
so records _must_ be special cased
<pikajude>
i think typescript has some good syntax for record types
<pikajude>
or purescript
<pikajude>
one of the two
<pikajude>
god knows what it was though
<drparse>
never even heard of purescript
<drparse>
oh it's like haskell
<pikajude>
wOH
<pikajude>
i think it was flow
<drparse>
wow impressive set of features
<pikajude>
that was it
<pikajude>
the one with record types
<drparse>
Algebraic data types, Pattern matching, Type inference, Type classes, Higher kinded types, Rank-N types, Extensible records, Extensible effects, Modules, Simple FFI, No runtime system, Human-readable output
<pikajude>
so instead of Foo { bar :: A, baz :: B } it's just { bar :: A, baz :: B }
<pikajude>
structural vs nominal typing
<drparse>
yes
<drparse>
why not both!
<pikajude>
nix needs structural typing
<drparse>
what's nix?
<pikajude>
package manager
<pikajude>
and other stuff
<drparse>
why does it need structural typing?
<pikajude>
because the package expressions are written in a language that is basically just hashmaps
<drparse>
hm
<pikajude>
and it's untyped
<pikajude>
{ foo = 1; bar = 2; }
<pikajude>
like that
<drparse>
json?
<pikajude>
actually, toJSON is a primitive
<pikajude>
but it's, you know, a language
<drparse>
I see
<pikajude>
it has function calls and all that
<drparse>
sooooooooo anywaaaaaaaaaaaaaaaaaaaaay
<pikajude>
soooooooooooooooooooooo
<drparse>
1. What are all the interfaces that we can have in our type system
<drparse>
type interfaces
<drparse>
so if you imagine a type system as a very boring and restrictive programming language, there's a certain set of operations and interfaces
<drparse>
e.g. getting a field is one of them
<drparse>
in a where clause
<drparse>
actually it's all about the where clauses right?
<drparse>
where <type>.<fieldname> is one kind of type interface. Object, String -> Object
<drparse>
another is equivalence. if two types have the same representation they are equivalent. but it's possible for two types to have different representations but still be equivalent
<drparse>
which appears in where clauses as: where T1 is T2
<drparse>
then there is compatibility (which is the same as equivalence, or not?). e.g. if you have a type at use and a type at declaration
<drparse>
e.g. passing in foo(Nat) to a function declared as foo :: Int
<drparse>
well Nat is a subset of Int so Nat ~> Int is compatible
<drparse>
I dunno how that works with where clauses though
<drparse>
foo<A>(A) where A ~> Int
<drparse>
I guess it's the mostly the same as equivalence
<drparse>
finally there's pattern matching
<drparse>
if you have a pattern (crudely) Foo<Bar<T, Int>>, how do you translate that into a where clause, and does it require any more type interfaces?
<drparse>
Foo { L1: Bar { L2: T, L3: $Int } } is our pattern
<drparse>
f<A, B>(A) where (A.L1.L2 ~> B and A.L1.L3 ~> $Int)
<drparse>
if it's structural
<drparse>
done?
drparse has quit [Quit: My MacBook Pro has gone to sleep. ZZZzzzβ¦]
alexgordon has joined #elliottcable
<alexgordon>
I guess it can't be structural
<alexgordon>
Array { Of: Type } vs Set { Of: Type }
<alexgordon>
the head matters
alexgordon is now known as drparse
<drparse>
so far we have type primatives ($Bool), type structures (Array { Of: Type }), type maps (\Set { Of: %T } -> Dict { Key: T, Val: $Void })
<drparse>
type predicates (HasLength) and type binary predicates (~>)
<drparse>
and record types
<drparse>
and two interfaces: 1. getting a named subtype (on record types and type structures), 2. type compatibility (~>)
<drparse>
and $methodMatching
<drparse>
I guess I can't spell primitive
<drparse>
and "subtype" here means more like "member type"
<drparse>
type of member
<drparse>
basically what I'm trying to do is merge the ideas from OCaml and Magpie, lol